# Metamath Proof Explorer

## Theorem opth

Description: The ordered pair theorem. If two ordered pairs are equal, their first elements are equal and their second elements are equal. Exercise 6 of TakeutiZaring p. 16. Note that C and D are not required to be sets due our specific ordered pair definition. (Contributed by NM, 28-May-1995)

Ref Expression
Hypotheses opth1.1
`|- A e. _V`
opth1.2
`|- B e. _V`
Assertion opth
`|- ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) )`

### Proof

Step Hyp Ref Expression
1 opth1.1
` |-  A e. _V`
2 opth1.2
` |-  B e. _V`
3 1 2 opth1
` |-  ( <. A , B >. = <. C , D >. -> A = C )`
4 1 2 opi1
` |-  { A } e. <. A , B >.`
5 id
` |-  ( <. A , B >. = <. C , D >. -> <. A , B >. = <. C , D >. )`
6 4 5 eleqtrid
` |-  ( <. A , B >. = <. C , D >. -> { A } e. <. C , D >. )`
7 oprcl
` |-  ( { A } e. <. C , D >. -> ( C e. _V /\ D e. _V ) )`
8 6 7 syl
` |-  ( <. A , B >. = <. C , D >. -> ( C e. _V /\ D e. _V ) )`
9 8 simprd
` |-  ( <. A , B >. = <. C , D >. -> D e. _V )`
10 3 opeq1d
` |-  ( <. A , B >. = <. C , D >. -> <. A , B >. = <. C , B >. )`
11 10 5 eqtr3d
` |-  ( <. A , B >. = <. C , D >. -> <. C , B >. = <. C , D >. )`
12 8 simpld
` |-  ( <. A , B >. = <. C , D >. -> C e. _V )`
13 dfopg
` |-  ( ( C e. _V /\ B e. _V ) -> <. C , B >. = { { C } , { C , B } } )`
14 12 2 13 sylancl
` |-  ( <. A , B >. = <. C , D >. -> <. C , B >. = { { C } , { C , B } } )`
15 11 14 eqtr3d
` |-  ( <. A , B >. = <. C , D >. -> <. C , D >. = { { C } , { C , B } } )`
16 dfopg
` |-  ( ( C e. _V /\ D e. _V ) -> <. C , D >. = { { C } , { C , D } } )`
17 8 16 syl
` |-  ( <. A , B >. = <. C , D >. -> <. C , D >. = { { C } , { C , D } } )`
18 15 17 eqtr3d
` |-  ( <. A , B >. = <. C , D >. -> { { C } , { C , B } } = { { C } , { C , D } } )`
19 prex
` |-  { C , B } e. _V`
20 prex
` |-  { C , D } e. _V`
21 19 20 preqr2
` |-  ( { { C } , { C , B } } = { { C } , { C , D } } -> { C , B } = { C , D } )`
22 18 21 syl
` |-  ( <. A , B >. = <. C , D >. -> { C , B } = { C , D } )`
23 preq2
` |-  ( x = D -> { C , x } = { C , D } )`
24 23 eqeq2d
` |-  ( x = D -> ( { C , B } = { C , x } <-> { C , B } = { C , D } ) )`
25 eqeq2
` |-  ( x = D -> ( B = x <-> B = D ) )`
26 24 25 imbi12d
` |-  ( x = D -> ( ( { C , B } = { C , x } -> B = x ) <-> ( { C , B } = { C , D } -> B = D ) ) )`
27 vex
` |-  x e. _V`
28 2 27 preqr2
` |-  ( { C , B } = { C , x } -> B = x )`
29 26 28 vtoclg
` |-  ( D e. _V -> ( { C , B } = { C , D } -> B = D ) )`
30 9 22 29 sylc
` |-  ( <. A , B >. = <. C , D >. -> B = D )`
31 3 30 jca
` |-  ( <. A , B >. = <. C , D >. -> ( A = C /\ B = D ) )`
32 opeq12
` |-  ( ( A = C /\ B = D ) -> <. A , B >. = <. C , D >. )`
33 31 32 impbii
` |-  ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) )`