Theorem altopthd

Description: Alternate ordered pair theorem with different sethood requirements. See altopth for more comments. (Contributed by Scott Fenton, 14-Apr-2012)

	Ref	Expression
Hypotheses	altopthd.1	|- C e. _V
	altopthd.2	|- D e. _V
Assertion	altopthd	|- ( << A , B >> = << C , D >> <-> ( A = C /\ B = D ) )

Proof

Step	Hyp	Ref	Expression
1		altopthd.1	|- C e. _V
2		altopthd.2	|- D e. _V
3		eqcom	|- ( << A , B >> = << C , D >> <-> << C , D >> = << A , B >> )
4	1 2	altopth	|- ( << C , D >> = << A , B >> <-> ( C = A /\ D = B ) )
5		eqcom	|- ( C = A <-> A = C )
6		eqcom	|- ( D = B <-> B = D )
7	5 6	anbi12i	|- ( ( C = A /\ D = B ) <-> ( A = C /\ B = D ) )
8	3 4 7	3bitri	|- ( << A , B >> = << C , D >> <-> ( A = C /\ B = D ) )