Proof
01. 1 ⊢ set x ∧ set y, hypo.
02. 1 ⊢ set x, conj_eliml 1.
03. 1 ⊢ set y, conj_elimr 1.
04. ⊢ ⋂(x, y) = ⋂(x, y), eq_refl.
05. ⊢ (x, y) = {{x}, {x, y}}, pair_eq.
06. ⊢ ⋂(x, y) = ⋂{{x}, {x, y}}, eq_subst 5 4, P u ↔ ⋂(x, y) = ⋂u.
07. 1 ⊢ set {x}, set_sg 2.
08. 1 ⊢ set {x, y}, pairing 2 3.
09. 1 ⊢ set {x} ∧ set {x, y}, conj_intro 7 8.
10. 1 ⊢ ⋂{{x}, {x, y}} = {x} ∩ {x, y}, Intersection_pair_set 9.
11. 1 ⊢ ⋂(x, y) = {x} ∩ {x, y}, eq_trans 6 10.
12. ⊢ {x} ⊆ {x, y}, union_incl_left.
13. ⊢ {x} ∩ {x, y} = {x}, intersection_from_incl 12.
14. 1 ⊢ ⋂(x, y) = {x}, eq_trans 11 13.
15. 1 ⊢ ⋂⋂(x, y) = ⋂{x}, f_equal 14, f u = ⋂u.
16. 1 ⊢ ⋂{x} = x, Intersection_sg 2.
17. 1 ⊢ ⋂⋂(x, y) = x, eq_trans 15 16.
18. ⊢ fst (x, y) = ⋂⋂(x, y), fst_eq.
19. 1 ⊢ fst (x, y) = x, eq_trans 18 17.
pair_fst_conj. ⊢ set x ∧ set y → fst (x, y) = x, subj_intro 19.
Dependencies
The given proof depends on five axioms:
comp, eq_refl, eq_subst, ext, pairing.