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

Theorem opth 4554
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 4553 . . 3  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  A  =  C )
41, 2opi1 4547 . . . . . . 7  |-  { A }  e.  <. A ,  B >.
5 id 22 . . . . . . 7  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. A ,  B >.  = 
<. C ,  D >. )
64, 5syl5eleq 2519 . . . . . 6  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  { A }  e.  <. C ,  D >. )
7 oprcl 4072 . . . . . 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 460 . . . 4  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  D  e.  _V )
103opeq1d 4053 . . . . . . . 8  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. A ,  B >.  = 
<. C ,  B >. )
1110, 5eqtr3d 2467 . . . . . . 7  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. C ,  B >.  = 
<. C ,  D >. )
128simpld 456 . . . . . . . 8  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  C  e.  _V )
13 dfopg 4045 . . . . . . . 8  |-  ( ( C  e.  _V  /\  B  e.  _V )  -> 
<. C ,  B >.  =  { { C } ,  { C ,  B } } )
1412, 2, 13sylancl 655 . . . . . . 7  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. C ,  B >.  =  { { C } ,  { C ,  B } } )
1511, 14eqtr3d 2467 . . . . . 6  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. C ,  D >.  =  { { C } ,  { C ,  B } } )
16 dfopg 4045 . . . . . . 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 2467 . . . . 5  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  { { C } ,  { C ,  B } }  =  { { C } ,  { C ,  D } } )
19 prex 4522 . . . . . 6  |-  { C ,  B }  e.  _V
20 prex 4522 . . . . . 6  |-  { C ,  D }  e.  _V
2119, 20preqr2 4035 . . . . 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 3943 . . . . . . 7  |-  ( x  =  D  ->  { C ,  x }  =  { C ,  D }
)
2423eqeq2d 2444 . . . . . 6  |-  ( x  =  D  ->  ( { C ,  B }  =  { C ,  x } 
<->  { C ,  B }  =  { C ,  D } ) )
25 eqeq2 2442 . . . . . 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 2965 . . . . . 6  |-  x  e. 
_V
282, 27preqr2 4035 . . . . 5  |-  ( { C ,  B }  =  { C ,  x }  ->  B  =  x )
2926, 28vtoclg 3019 . . . 4  |-  ( D  e.  _V  ->  ( { C ,  B }  =  { C ,  D }  ->  B  =  D ) )
309, 22, 29sylc 60 . . 3  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  B  =  D )
313, 30jca 529 . 2  |-  ( <. A ,  B >.  = 
<. C ,  D >.  -> 
( A  =  C  /\  B  =  D ) )
32 opeq12 4049 . 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 1362    e. wcel 1755   _Vcvv 2962   {csn 3865   {cpr 3867   <.cop 3871
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872
This theorem is referenced by:  opthg  4555  otth2  4561  copsexg  4564  copsexgOLD  4565  copsex4g  4568  opcom  4573  moop2  4574  opelopabsbOLD  4586  ralxpf  4973  cnvcnvsn  5304  funopg  5438  xpopth  6604  eqop  6605  opiota  6622  soxp  6674  fnwelem  6676  xpdom2  7394  xpf1o  7461  unxpdomlem2  7506  unxpdomlem3  7507  xpwdomg  7788  fseqenlem1  8182  iundom2g  8692  eqresr  9292  cnref1o  10974  hashfun  12183  fsumcom2  13225  xpnnenOLD  13475  qredeu  13776  qnumdenbi  13805  crt  13836  prmreclem3  13962  imasaddfnlem  14449  dprd2da  16515  dprd2d2  16517  ucnima  19698  br8d  25766  xppreima2  25789  ofpreima  25808  erdszelem9  26935  fprodcom2  27342  brtp  27406  br8  27413  br6  27414  br4  27415  brsegle  27986  f1opr  28462  pellexlem3  29017  pellex  29021  oprabv  30003  numclwlk1lem2f1  30533  opelopab4  30961  dib1dim  34383  diclspsn  34412  dihopelvalcpre  34466  dihmeetlem4preN  34524  dihmeetlem13N  34537  dih1dimatlem  34547  dihatlat  34552
  Copyright terms: Public domain W3C validator