Proof 01. 1 ⊢ set x ∧ set y, hypo. 02. 2 ⊢ (x, y) = (x', y'), hypo. 03. 1 ⊢ set x, conj_eliml 1. 04. 1 ⊢ set y, conj_elimr 1. 05. 1 ⊢ set (x, y), set_pair 3 4. 06. 1, 2 ⊢ set (x', y'), eq_subst 2 5, P u ↔ set u. 07. 1, 2 ⊢ set x', setl_from_pair 6. 08. 1, 2 ⊢ set y', setr_from_pair 6. 09. 1, 2 ⊢ set x' ∧ set y', conj_intro 7 8. 10. 2 ⊢ fst (x, y) = fst (x', y'), f_equal 2, f u = fst u. 11. 1 ⊢ fst (x, y) = x, pair_fst_conj 1. 12. 1 ⊢ x = fst (x, y), eq_symm 11. 13. 1, 2 ⊢ fst (x', y') = x', pair_fst_conj 9. 14. 1, 2 ⊢ x = fst (x', y'), eq_trans 12 10. 15. 1, 2 ⊢ x = x', eq_trans 14 13. 16. 2 ⊢ scd (x, y) = scd (x', y'), f_equal 2, f u = scd u. 17. 1 ⊢ scd (x, y) = y, pair_scd_conj 1. 18. 1 ⊢ y = scd (x, y), eq_symm 17. 19. 1, 2 ⊢ scd (x', y') = y', pair_scd_conj 9. 20. 1, 2 ⊢ y = scd (x', y'), eq_trans 18 16. 21. 1, 2 ⊢ y = y', eq_trans 20 19. 22. 1, 2 ⊢ x = x' ∧ y = y', conj_intro 15 21. pair_property_conj. ⊢ set x ∧ set y → (x, y) = (x', y') → x = x' ∧ y = y', subj_intro_ii 22.
Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.