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

Theorem recnprss 19270
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 3673 . 2  |-  ( S  e.  { RR ,  CC }  ->  ( S  =  RR  \/  S  =  CC ) )
2 ax-resscn 8810 . . . 4  |-  RR  C_  CC
3 sseq1 3212 . . . 4  |-  ( S  =  RR  ->  ( S  C_  CC  <->  RR  C_  CC ) )
42, 3mpbiri 224 . . 3  |-  ( S  =  RR  ->  S  C_  CC )
5 eqimss 3243 . . 3  |-  ( S  =  CC  ->  S  C_  CC )
64, 5jaoi 368 . 2  |-  ( ( S  =  RR  \/  S  =  CC )  ->  S  C_  CC )
71, 6syl 15 1  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357    = wceq 1632    e. wcel 1696    C_ wss 3165   {cpr 3654   CCcc 8751   RRcr 8752
This theorem is referenced by:  dvres3  19279  dvres3a  19280  dvcnp  19284  dvnff  19288  dvnadd  19294  dvnres  19296  cpnord  19300  cpncn  19301  cpnres  19302  dvadd  19305  dvmul  19306  dvaddf  19307  dvmulf  19308  dvcmul  19309  dvcmulf  19310  dvco  19312  dvcof  19313  dvmptid  19322  dvmptc  19323  dvmptres2  19327  dvmptcmul  19329  dvmptfsum  19338  dvcnvlem  19339  dvcnv  19340  dvlip2  19358  taylfvallem1  19752  tayl0  19757  taylply2  19763  taylply  19764  dvtaylp  19765  dvntaylp  19766  taylthlem1  19768  ulmdvlem1  19793  ulmdvlem3  19795  ulmdv  19796  dvsconst  27650  dvsid  27651  dvsef  27652  dvconstbi  27654  expgrowth  27655
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-resscn 8810
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-in 3172  df-ss 3179  df-sn 3659  df-pr 3660
  Copyright terms: Public domain W3C validator