Metamath Proof Explorer

Theorem altopth

Description: The alternate ordered pair theorem. If two alternate ordered pairs are equal, their first elements are equal and their second elements are equal. Note that C and D are not required to be a set due to a peculiarity of our specific ordered pair definition, as opposed to the regular ordered pairs used here, which (as in opth ), requires D to be a set. (Contributed by Scott Fenton, 23-Mar-2012)

Ref Expression
Hypotheses altopth.1 ⊢ A ∈ V
altopth.2 ⊢ B ∈ V
Assertion altopth ⊢ A B = C D ↔ A = C ∧ B = D

Proof

Step Hyp Ref Expression
1 altopth.1 ⊢ A ∈ V
2 altopth.2 ⊢ B ∈ V
3 altopthg ⊢ A ∈ V ∧ B ∈ V → A B = C D ↔ A = C ∧ B = D
4 1 2 3 mp2an ⊢ A B = C D ↔ A = C ∧ B = D