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 ⊢AB=CD↔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→AB=CD↔A=C∧B=D
4 1 2 3 mp2an ⊢AB=CD↔A=C∧B=D