Theorem altopthb

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

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

Proof

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