Proof
01. 1 ⊢ set x ∧ set y, hypo.
02. 1 ⊢ set x, conj_eliml 1.
03. 1 ⊢ set y, conj_elimr 1.
04. 1 ⊢ x ∈ {x, y}, in21 2.
05. 1 ⊢ y ∈ {x, y}, in22 3.
06. 6 ⊢ u ∈ ⋂{x, y}, hypo.
07. 1, 6 ⊢ u ∈ x, Intersection_elim 6 4.
08. 1, 6 ⊢ u ∈ y, Intersection_elim 6 5.
09. 1, 6 ⊢ u ∈ x ∩ y, intersection_intro 7 8.
10. 1 ⊢ u ∈ ⋂{x, y} → u ∈ x ∩ y, subj_intro 9.
11. 1 ⊢ ∀u. u ∈ ⋂{x, y} → u ∈ x ∩ y, uq_intro 10.
12. 1 ⊢ ⋂{x, y} ⊆ x ∩ y, incl_intro 11.
13. 13 ⊢ u ∈ x ∩ y, hypo.
14. 13 ⊢ u ∈ x, intersection_eliml 13.
15. 13 ⊢ u ∈ y, intersection_elimr 13.
16. 13 ⊢ set u, set_intro 13.
17. 17 ⊢ a ∈ {x, y}, hypo.
18. 17 ⊢ a ∈ {x} ∨ a ∈ {y}, union_elim 17.
19. 19 ⊢ a ∈ {x}, hypo.
20. 1, 19 ⊢ a = x, sg_elim 2 19.
21. 1, 13, 19 ⊢ u ∈ a, eq_subst_rev 20 14, P x ↔ u ∈ x.
22. 22 ⊢ a ∈ {y}, hypo.
23. 1, 22 ⊢ a = y, sg_elim 3 22.
24. 1, 13, 22 ⊢ u ∈ a, eq_subst_rev 23 15, P x ↔ u ∈ x.
25. 1, 13, 17 ⊢ u ∈ a, disj_elim 18 21 24.
26. 1, 13 ⊢ a ∈ {x, y} → u ∈ a, subj_intro 25.
27. 1, 13 ⊢ ∀a. a ∈ {x, y} → u ∈ a, uq_intro 26.
28. 1, 13 ⊢ u ∈ ⋂{x, y}, Intersection_intro 16 27.
29. 1 ⊢ u ∈ x ∩ y → u ∈ ⋂{x, y}, subj_intro 28.
30. 1 ⊢ ∀u. u ∈ x ∩ y → u ∈ ⋂{x, y}, uq_intro 29.
31. 1 ⊢ x ∩ y ⊆ ⋂{x, y}, incl_intro 30.
32. 1 ⊢ ⋂{x, y} = x ∩ y, incl_antisym 12 31.
Intersection_pair_set. ⊢ set x ∧ set y → ⋂{x, y} = x ∩ y,
subj_intro 32.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.