pair_property

Theorem pair_property

Theorem. pair_property
set x → set y → (x, y) = (x', y') → x = x' ∧ y = y'

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 ⊢ (x, y) = (x', y') → x = x' ∧ y = y', pair_property_conj 3.
pair_property. ⊢ set x → set y → (x, y) = (x', y') → x = x' ∧ y = y',
  subj_intro_ii 4.

Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.