Theorem altopthbg

Description: Alternate ordered pair theorem. (Contributed by Scott Fenton, 14-Apr-2012)

	Ref	Expression
Assertion	altopthbg	|- ( ( A e. V /\ D e. W ) -> ( << A , B >> = << C , D >> <-> ( A = C /\ B = D ) ) )

Proof

Step	Hyp	Ref	Expression
1		altopthsn	|- ( << A , B >> = << C , D >> <-> ( { A } = { C } /\ { B } = { D } ) )
2		sneqbg	|- ( A e. V -> ( { A } = { C } <-> A = C ) )
3		sneqbg	|- ( D e. W -> ( { D } = { B } <-> D = B ) )
4		eqcom	|- ( { B } = { D } <-> { D } = { B } )
5		eqcom	|- ( B = D <-> D = B )
6	3 4 5	3bitr4g	|- ( D e. W -> ( { B } = { D } <-> B = D ) )
7	2 6	bi2anan9	|- ( ( A e. V /\ D e. W ) -> ( ( { A } = { C } /\ { B } = { D } ) <-> ( A = C /\ B = D ) ) )
8	1 7	bitrid	|- ( ( A e. V /\ D e. W ) -> ( << A , B >> = << C , D >> <-> ( A = C /\ B = D ) ) )