MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opth Structured version   Unicode version

Theorem opth 4714
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.)
Hypotheses
Ref Expression
opth1.1  |-  A  e. 
_V
opth1.2  |-  B  e. 
_V
Assertion
Ref Expression
opth  |-  ( <. A ,  B >.  = 
<. C ,  D >.  <->  ( A  =  C  /\  B  =  D )
)

Proof of Theorem opth
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 opth1.1 . . . 4  |-  A  e. 
_V
2 opth1.2 . . . 4  |-  B  e. 
_V
31, 2opth1 4713 . . 3  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  A  =  C )
41, 2opi1 4707 . . . . . . 7  |-  { A }  e.  <. A ,  B >.
5 id 22 . . . . . . 7  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. A ,  B >.  = 
<. C ,  D >. )
64, 5syl5eleq 2554 . . . . . 6  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  { A }  e.  <. C ,  D >. )
7 oprcl 4231 . . . . . 6  |-  ( { A }  e.  <. C ,  D >.  ->  ( C  e.  _V  /\  D  e.  _V ) )
86, 7syl 16 . . . . 5  |-  ( <. A ,  B >.  = 
<. C ,  D >.  -> 
( C  e.  _V  /\  D  e.  _V )
)
98simprd 463 . . . 4  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  D  e.  _V )
103opeq1d 4212 . . . . . . . 8  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. A ,  B >.  = 
<. C ,  B >. )
1110, 5eqtr3d 2503 . . . . . . 7  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. C ,  B >.  = 
<. C ,  D >. )
128simpld 459 . . . . . . . 8  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  C  e.  _V )
13 dfopg 4204 . . . . . . . 8  |-  ( ( C  e.  _V  /\  B  e.  _V )  -> 
<. C ,  B >.  =  { { C } ,  { C ,  B } } )
1412, 2, 13sylancl 662 . . . . . . 7  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. C ,  B >.  =  { { C } ,  { C ,  B } } )
1511, 14eqtr3d 2503 . . . . . 6  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. C ,  D >.  =  { { C } ,  { C ,  B } } )
16 dfopg 4204 . . . . . . 7  |-  ( ( C  e.  _V  /\  D  e.  _V )  -> 
<. C ,  D >.  =  { { C } ,  { C ,  D } } )
178, 16syl 16 . . . . . 6  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. C ,  D >.  =  { { C } ,  { C ,  D } } )
1815, 17eqtr3d 2503 . . . . 5  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  { { C } ,  { C ,  B } }  =  { { C } ,  { C ,  D } } )
19 prex 4682 . . . . . 6  |-  { C ,  B }  e.  _V
20 prex 4682 . . . . . 6  |-  { C ,  D }  e.  _V
2119, 20preqr2 4194 . . . . 5  |-  ( { { C } ,  { C ,  B } }  =  { { C } ,  { C ,  D } }  ->  { C ,  B }  =  { C ,  D } )
2218, 21syl 16 . . . 4  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  { C ,  B }  =  { C ,  D } )
23 preq2 4100 . . . . . . 7  |-  ( x  =  D  ->  { C ,  x }  =  { C ,  D }
)
2423eqeq2d 2474 . . . . . 6  |-  ( x  =  D  ->  ( { C ,  B }  =  { C ,  x } 
<->  { C ,  B }  =  { C ,  D } ) )
25 eqeq2 2475 . . . . . 6  |-  ( x  =  D  ->  ( B  =  x  <->  B  =  D ) )
2624, 25imbi12d 320 . . . . 5  |-  ( x  =  D  ->  (
( { C ,  B }  =  { C ,  x }  ->  B  =  x )  <-> 
( { C ,  B }  =  { C ,  D }  ->  B  =  D ) ) )
27 vex 3109 . . . . . 6  |-  x  e. 
_V
282, 27preqr2 4194 . . . . 5  |-  ( { C ,  B }  =  { C ,  x }  ->  B  =  x )
2926, 28vtoclg 3164 . . . 4  |-  ( D  e.  _V  ->  ( { C ,  B }  =  { C ,  D }  ->  B  =  D ) )
309, 22, 29sylc 60 . . 3  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  B  =  D )
313, 30jca 532 . 2  |-  ( <. A ,  B >.  = 
<. C ,  D >.  -> 
( A  =  C  /\  B  =  D ) )
32 opeq12 4208 . 2  |-  ( ( A  =  C  /\  B  =  D )  -> 
<. A ,  B >.  = 
<. C ,  D >. )
3331, 32impbii 188 1  |-  ( <. A ,  B >.  = 
<. C ,  D >.  <->  ( A  =  C  /\  B  =  D )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1374    e. wcel 1762   _Vcvv 3106   {csn 4020   {cpr 4022   <.cop 4026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027
This theorem is referenced by:  opthg  4715  otth2  4721  copsexg  4725  copsexgOLD  4726  copsex4g  4729  opcom  4734  moop2  4735  opelopabsbALT  4749  ralxpf  5140  cnvcnvsn  5476  funopg  5611  oprabv  6320  xpopth  6813  eqop  6814  opiota  6833  soxp  6886  fnwelem  6888  xpdom2  7602  xpf1o  7669  unxpdomlem2  7715  unxpdomlem3  7716  xpwdomg  8000  fseqenlem1  8394  iundom2g  8904  eqresr  9503  cnref1o  11204  hashfun  12448  fsumcom2  13538  xpnnenOLD  13793  qredeu  14096  qnumdenbi  14125  crt  14156  prmreclem3  14284  imasaddfnlem  14772  dprd2da  16874  dprd2d2  16876  ucnima  20512  br8d  26986  xppreima2  27010  ofpreima  27029  erdszelem9  28133  fprodcom2  28541  brtp  28605  br8  28612  br6  28613  br4  28614  brsegle  29185  f1opr  29669  pellexlem3  30222  pellex  30226  numclwlk1lem2f1  31813  opelopab4  32279  dib1dim  35837  diclspsn  35866  dihopelvalcpre  35920  dihmeetlem4preN  35978  dihmeetlem13N  35991  dih1dimatlem  36001  dihatlat  36006
  Copyright terms: Public domain W3C validator