Proof
01. 1 ⊢ set a, hypo.
02. 2 ⊢ x ∈ ⋂{a}, hypo.
03. ⊢ a = a, eq_refl.
04. 1 ⊢ a ∈ {a}, sg_intro 1 3.
05. 1, 2 ⊢ x ∈ a, Intersection_elim 2 4.
06. 1 ⊢ x ∈ ⋂{a} → x ∈ a, subj_intro 5.
07. 1 ⊢ ∀x. x ∈ ⋂{a} → x ∈ a, uq_intro 6.
08. 1 ⊢ ⋂{a} ⊆ a, incl_intro 7.
09. 9 ⊢ x ∈ a, hypo.
10. 10 ⊢ y ∈ {a}, hypo.
11. 1, 10 ⊢ y = a, sg_elim 1 10.
12. 1, 9, 10 ⊢ x ∈ y, eq_subst_rev 11 9, P u ↔ x ∈ u.
13. 1, 9 ⊢ y ∈ {a} → x ∈ y, subj_intro 12.
14. 1, 9 ⊢ ∀y. y ∈ {a} → x ∈ y, uq_intro 13.
15. 9 ⊢ set x, set_intro 9.
16. 1, 9 ⊢ x ∈ ⋂{a}, Intersection_intro 15 14.
17. 1 ⊢ x ∈ a → x ∈ ⋂{a}, subj_intro 16.
18. 1 ⊢ ∀x. x ∈ a → x ∈ ⋂{a}, uq_intro 17.
19. 1 ⊢ a ⊆ ⋂{a}, incl_intro 18.
20. 1 ⊢ ⋂{a} = a, incl_antisym 8 19.
Intersection_sg. ⊢ set a → ⋂{a} = a, subj_intro 20.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.