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

Theorem dfcnqs 9517
Description: Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in  CC from those in  R.. The trick involves qsid 7384, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) acts as an identity divisor for the quotient set operation. This lets us "pretend" that  CC is a quotient set, even though it is not (compare df-c 9496), and allows us to reuse some of the equivalence class lemmas we developed for the transition from positive reals to signed reals, etc. (Contributed by NM, 13-Aug-1995.) (New usage is discouraged.)
Assertion
Ref Expression
dfcnqs  |-  CC  =  ( ( R.  X.  R. ) /. `'  _E  )

Proof of Theorem dfcnqs
StepHypRef Expression
1 df-c 9496 . 2  |-  CC  =  ( R.  X.  R. )
2 qsid 7384 . 2  |-  ( ( R.  X.  R. ) /. `'  _E  )  =  ( R.  X.  R. )
31, 2eqtr4i 2453 1  |-  CC  =  ( ( R.  X.  R. ) /. `'  _E  )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    _E cep 4705    X. cxp 4794   `'ccnv 4795   /.cqs 7317   R.cnr 9241   CCcc 9488
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pr 4603
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-sbc 3243  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-br 4367  df-opab 4426  df-eprel 4707  df-xp 4802  df-cnv 4804  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-ec 7320  df-qs 7324  df-c 9496
This theorem is referenced by:  axmulcom  9530  axaddass  9531  axmulass  9532  axdistr  9533
  Copyright terms: Public domain W3C validator