Proof 01. 1 ⊢ set x, hypo. 02. 2 ⊢ set y, hypo. 03. 1, 2 ⊢ set x ∧ set y, conj_intro 1 2. 04. 1, 2 ⊢ fst (x, y) = x, pair_fst_conj 3. pair_fst. ⊢ set x → set y → fst (x, y) = x, subj_intro_ii 4.
Dependencies
The given proof depends on five axioms:
comp, eq_refl, eq_subst, ext, pairing.