Theorem altopthc

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

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

Proof

Step	Hyp	Ref	Expression
1		altopthc.1	|- B e. _V
2		altopthc.2	|- C e. _V
3		eqcom	|- ( << A , B >> = << C , D >> <-> << C , D >> = << A , B >> )
4	2 1	altopthb	|- ( << 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 ) )