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

Theorem opth 4561
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 4560 . . 3  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  A  =  C )
41, 2opi1 4554 . . . . . . 7  |-  { A }  e.  <. A ,  B >.
5 id 22 . . . . . . 7  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. A ,  B >.  = 
<. C ,  D >. )
64, 5syl5eleq 2524 . . . . . 6  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  { A }  e.  <. C ,  D >. )
7 oprcl 4079 . . . . . 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 4060 . . . . . . . 8  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. A ,  B >.  = 
<. C ,  B >. )
1110, 5eqtr3d 2472 . . . . . . 7  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. C ,  B >.  = 
<. C ,  D >. )
128simpld 459 . . . . . . . 8  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  C  e.  _V )
13 dfopg 4052 . . . . . . . 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 2472 . . . . . 6  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. C ,  D >.  =  { { C } ,  { C ,  B } } )
16 dfopg 4052 . . . . . . 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 2472 . . . . 5  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  { { C } ,  { C ,  B } }  =  { { C } ,  { C ,  D } } )
19 prex 4529 . . . . . 6  |-  { C ,  B }  e.  _V
20 prex 4529 . . . . . 6  |-  { C ,  D }  e.  _V
2119, 20preqr2 4042 . . . . 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 3950 . . . . . . 7  |-  ( x  =  D  ->  { C ,  x }  =  { C ,  D }
)
2423eqeq2d 2449 . . . . . 6  |-  ( x  =  D  ->  ( { C ,  B }  =  { C ,  x } 
<->  { C ,  B }  =  { C ,  D } ) )
25 eqeq2 2447 . . . . . 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 2970 . . . . . 6  |-  x  e. 
_V
282, 27preqr2 4042 . . . . 5  |-  ( { C ,  B }  =  { C ,  x }  ->  B  =  x )
2926, 28vtoclg 3025 . . . 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 4056 . 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 1369    e. wcel 1756   _Vcvv 2967   {csn 3872   {cpr 3874   <.cop 3878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879
This theorem is referenced by:  opthg  4562  otth2  4568  copsexg  4571  copsexgOLD  4572  copsex4g  4575  opcom  4580  moop2  4581  opelopabsbALT  4593  ralxpf  4981  cnvcnvsn  5311  funopg  5445  xpopth  6610  eqop  6611  opiota  6628  soxp  6680  fnwelem  6682  xpdom2  7398  xpf1o  7465  unxpdomlem2  7510  unxpdomlem3  7511  xpwdomg  7792  fseqenlem1  8186  iundom2g  8696  eqresr  9296  cnref1o  10978  hashfun  12191  fsumcom2  13233  xpnnenOLD  13484  qredeu  13785  qnumdenbi  13814  crt  13845  prmreclem3  13971  imasaddfnlem  14458  dprd2da  16531  dprd2d2  16533  ucnima  19836  br8d  25910  xppreima2  25933  ofpreima  25952  erdszelem9  27056  fprodcom2  27464  brtp  27528  br8  27535  br6  27536  br4  27537  brsegle  28108  f1opr  28589  pellexlem3  29143  pellex  29147  oprabv  30128  numclwlk1lem2f1  30658  opelopab4  31189  dib1dim  34703  diclspsn  34732  dihopelvalcpre  34786  dihmeetlem4preN  34844  dihmeetlem13N  34857  dih1dimatlem  34867  dihatlat  34872
  Copyright terms: Public domain W3C validator