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

Theorem recnprss 21338
Description: Both  RR and  CC are subsets of  CC. (Contributed by Mario Carneiro, 10-Feb-2015.)
Assertion
Ref Expression
recnprss  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )

Proof of Theorem recnprss
StepHypRef Expression
1 elpri 3894 . 2  |-  ( S  e.  { RR ,  CC }  ->  ( S  =  RR  \/  S  =  CC ) )
2 ax-resscn 9335 . . . 4  |-  RR  C_  CC
3 sseq1 3374 . . . 4  |-  ( S  =  RR  ->  ( S  C_  CC  <->  RR  C_  CC ) )
42, 3mpbiri 233 . . 3  |-  ( S  =  RR  ->  S  C_  CC )
5 eqimss 3405 . . 3  |-  ( S  =  CC  ->  S  C_  CC )
64, 5jaoi 379 . 2  |-  ( ( S  =  RR  \/  S  =  CC )  ->  S  C_  CC )
71, 6syl 16 1  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 368    = wceq 1364    e. wcel 1761    C_ wss 3325   {cpr 3876   CCcc 9276   RRcr 9277
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 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-resscn 9335
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-un 3330  df-in 3332  df-ss 3339  df-sn 3875  df-pr 3877
This theorem is referenced by:  dvres3  21347  dvres3a  21348  dvcnp  21352  dvnff  21356  dvnadd  21362  dvnres  21364  cpnord  21368  cpncn  21369  cpnres  21370  dvadd  21373  dvmul  21374  dvaddf  21375  dvmulf  21376  dvcmul  21377  dvcmulf  21378  dvco  21380  dvcof  21381  dvmptid  21390  dvmptc  21391  dvmptres2  21395  dvmptcmul  21397  dvmptfsum  21406  dvcnvlem  21407  dvcnv  21408  dvlip2  21426  taylfvallem1  21781  tayl0  21786  taylply2  21792  taylply  21793  dvtaylp  21794  dvntaylp  21795  taylthlem1  21797  ulmdvlem1  21824  ulmdvlem3  21826  ulmdv  21827  dvsconst  29529  dvsid  29530  dvsef  29531  dvconstbi  29533  expgrowth  29534
  Copyright terms: Public domain W3C validator