Theorem opthg2

Description: Ordered pair theorem. (Contributed by NM, 14-Oct-2005) (Revised by Mario Carneiro, 26-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		opthg	|- ( ( C e. V /\ D e. W ) -> ( <. C , D >. = <. A , B >. <-> ( C = A /\ D = B ) ) )
2		eqcom	|- ( <. A , B >. = <. C , D >. <-> <. C , D >. = <. A , B >. )
3		eqcom	|- ( A = C <-> C = A )
4		eqcom	|- ( B = D <-> D = B )
5	3 4	anbi12i	|- ( ( A = C /\ B = D ) <-> ( C = A /\ D = B ) )
6	1 2 5	3bitr4g	|- ( ( C e. V /\ D e. W ) -> ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) ) )