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. 06. 1, 2 ⊢ scd (x, y) = y, pair_scd_conj 3. pair_scd. ⊢ set x → set y → scd (x, y) = y, subj_intro_ii 6.
Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing.