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