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

Theorem opth 4679
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 4678 . . 3  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  A  =  C )
41, 2opi1 4672 . . . . . . 7  |-  { A }  e.  <. A ,  B >.
5 id 22 . . . . . . 7  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. A ,  B >.  = 
<. C ,  D >. )
64, 5syl5eleq 2537 . . . . . 6  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  { A }  e.  <. C ,  D >. )
7 oprcl 4194 . . . . . 6  |-  ( { A }  e.  <. C ,  D >.  ->  ( C  e.  _V  /\  D  e.  _V ) )
86, 7syl 17 . . . . 5  |-  ( <. A ,  B >.  = 
<. C ,  D >.  -> 
( C  e.  _V  /\  D  e.  _V )
)
98simprd 465 . . . 4  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  D  e.  _V )
103opeq1d 4175 . . . . . . . 8  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. A ,  B >.  = 
<. C ,  B >. )
1110, 5eqtr3d 2489 . . . . . . 7  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. C ,  B >.  = 
<. C ,  D >. )
128simpld 461 . . . . . . . 8  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  C  e.  _V )
13 dfopg 4167 . . . . . . . 8  |-  ( ( C  e.  _V  /\  B  e.  _V )  -> 
<. C ,  B >.  =  { { C } ,  { C ,  B } } )
1412, 2, 13sylancl 669 . . . . . . 7  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. C ,  B >.  =  { { C } ,  { C ,  B } } )
1511, 14eqtr3d 2489 . . . . . 6  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. C ,  D >.  =  { { C } ,  { C ,  B } } )
16 dfopg 4167 . . . . . . 7  |-  ( ( C  e.  _V  /\  D  e.  _V )  -> 
<. C ,  D >.  =  { { C } ,  { C ,  D } } )
178, 16syl 17 . . . . . 6  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. C ,  D >.  =  { { C } ,  { C ,  D } } )
1815, 17eqtr3d 2489 . . . . 5  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  { { C } ,  { C ,  B } }  =  { { C } ,  { C ,  D } } )
19 prex 4645 . . . . . 6  |-  { C ,  B }  e.  _V
20 prex 4645 . . . . . 6  |-  { C ,  D }  e.  _V
2119, 20preqr2 4153 . . . . 5  |-  ( { { C } ,  { C ,  B } }  =  { { C } ,  { C ,  D } }  ->  { C ,  B }  =  { C ,  D } )
2218, 21syl 17 . . . 4  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  { C ,  B }  =  { C ,  D } )
23 preq2 4055 . . . . . . 7  |-  ( x  =  D  ->  { C ,  x }  =  { C ,  D }
)
2423eqeq2d 2463 . . . . . 6  |-  ( x  =  D  ->  ( { C ,  B }  =  { C ,  x } 
<->  { C ,  B }  =  { C ,  D } ) )
25 eqeq2 2464 . . . . . 6  |-  ( x  =  D  ->  ( B  =  x  <->  B  =  D ) )
2624, 25imbi12d 322 . . . . 5  |-  ( x  =  D  ->  (
( { C ,  B }  =  { C ,  x }  ->  B  =  x )  <-> 
( { C ,  B }  =  { C ,  D }  ->  B  =  D ) ) )
27 vex 3050 . . . . . 6  |-  x  e. 
_V
282, 27preqr2 4153 . . . . 5  |-  ( { C ,  B }  =  { C ,  x }  ->  B  =  x )
2926, 28vtoclg 3109 . . . 4  |-  ( D  e.  _V  ->  ( { C ,  B }  =  { C ,  D }  ->  B  =  D ) )
309, 22, 29sylc 62 . . 3  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  B  =  D )
313, 30jca 535 . 2  |-  ( <. A ,  B >.  = 
<. C ,  D >.  -> 
( A  =  C  /\  B  =  D ) )
32 opeq12 4171 . 2  |-  ( ( A  =  C  /\  B  =  D )  -> 
<. A ,  B >.  = 
<. C ,  D >. )
3331, 32impbii 191 1  |-  ( <. A ,  B >.  = 
<. C ,  D >.  <->  ( A  =  C  /\  B  =  D )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1446    e. wcel 1889   _Vcvv 3047   {csn 3970   {cpr 3972   <.cop 3976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pr 4642
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-rab 2748  df-v 3049  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977
This theorem is referenced by:  opthg  4680  otth2  4686  copsexg  4690  copsex4g  4693  opcom  4698  moop2  4699  opelopabsbALT  4713  ralxpf  4984  cnvcnvsn  5316  funopg  5617  tpres  6122  oprabv  6344  xpopth  6837  eqop  6838  opiota  6857  soxp  6914  fnwelem  6916  xpdom2  7672  xpf1o  7739  unxpdomlem2  7782  unxpdomlem3  7783  xpwdomg  8105  fseqenlem1  8460  iundom2g  8970  eqresr  9566  cnref1o  11304  hashfun  12616  fsumcom2  13847  fprodcom2  14050  qredeu  14676  qnumdenbi  14705  crt  14738  prmreclem3  14874  imasaddfnlem  15446  dprd2da  17687  dprd2d2  17689  ucnima  21308  numclwlk1lem2f1  25834  br8d  28230  xppreima2  28261  aciunf1lem  28276  ofpreima  28280  erdszelem9  29934  msubff1  30206  mvhf1  30209  brtp  30401  br8  30408  br6  30409  br4  30410  brsegle  30887  poimirlem4  31956  poimirlem9  31961  f1opr  32063  dib1dim  34745  diclspsn  34774  dihopelvalcpre  34828  dihmeetlem4preN  34886  dihmeetlem13N  34899  dih1dimatlem  34909  dihatlat  34914  pellexlem3  35687  pellex  35691  snhesn  36394  opelopab4  36929  propssopi  39010  funsndifnop  39032
  Copyright terms: Public domain W3C validator