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 e. _V
	altopth.2	|- B e. _V
Assertion	altopth	|- ( << A , B >> = << C , D >> <-> ( A = C /\ B = D ) )

Proof

Step	Hyp	Ref	Expression
1		altopth.1	|- A e. _V
2		altopth.2	|- B e. _V
3		altopthg	|- ( ( A e. _V /\ B e. _V ) -> ( << A , B >> = << C , D >> <-> ( A = C /\ B = D ) ) )
4	1 2 3	mp2an	|- ( << A , B >> = << C , D >> <-> ( A = C /\ B = D ) )