This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )