Theorem opthg

Description: Ordered pair theorem. C and D are not required to be sets under our specific ordered pair definition. (Contributed by NM, 14-Oct-2005) (Revised by Mario Carneiro, 26-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		opeq1	|- ( x = A -> <. x , y >. = <. A , y >. )
2	1	eqeq1d	|- ( x = A -> ( <. x , y >. = <. C , D >. <-> <. A , y >. = <. C , D >. ) )
3		eqeq1	|- ( x = A -> ( x = C <-> A = C ) )
4	3	anbi1d	|- ( x = A -> ( ( x = C /\ y = D ) <-> ( A = C /\ y = D ) ) )
5	2 4	bibi12d	|- ( x = A -> ( ( <. x , y >. = <. C , D >. <-> ( x = C /\ y = D ) ) <-> ( <. A , y >. = <. C , D >. <-> ( A = C /\ y = D ) ) ) )
6		opeq2	|- ( y = B -> <. A , y >. = <. A , B >. )
7	6	eqeq1d	|- ( y = B -> ( <. A , y >. = <. C , D >. <-> <. A , B >. = <. C , D >. ) )
8		eqeq1	|- ( y = B -> ( y = D <-> B = D ) )
9	8	anbi2d	|- ( y = B -> ( ( A = C /\ y = D ) <-> ( A = C /\ B = D ) ) )
10	7 9	bibi12d	|- ( y = B -> ( ( <. A , y >. = <. C , D >. <-> ( A = C /\ y = D ) ) <-> ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) ) ) )
11		vex	|- x e. _V
12		vex	|- y e. _V
13	11 12	opth	|- ( <. x , y >. = <. C , D >. <-> ( x = C /\ y = D ) )
14	5 10 13	vtocl2g	|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) ) )