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

Theorem recnprss 19254
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 3660 . 2  |-  ( S  e.  { RR ,  CC }  ->  ( S  =  RR  \/  S  =  CC ) )
2 ax-resscn 8794 . . . 4  |-  RR  C_  CC
3 sseq1 3199 . . . 4  |-  ( S  =  RR  ->  ( S  C_  CC  <->  RR  C_  CC ) )
42, 3mpbiri 224 . . 3  |-  ( S  =  RR  ->  S  C_  CC )
5 eqimss 3230 . . 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 1623    e. wcel 1684    C_ wss 3152   {cpr 3641   CCcc 8735   RRcr 8736
This theorem is referenced by:  dvres3  19263  dvres3a  19264  dvcnp  19268  dvnff  19272  dvnadd  19278  dvnres  19280  cpnord  19284  cpncn  19285  cpnres  19286  dvadd  19289  dvmul  19290  dvaddf  19291  dvmulf  19292  dvcmul  19293  dvcmulf  19294  dvco  19296  dvcof  19297  dvmptid  19306  dvmptc  19307  dvmptres2  19311  dvmptcmul  19313  dvmptfsum  19322  dvcnvlem  19323  dvcnv  19324  dvlip2  19342  taylfvallem1  19736  tayl0  19741  taylply2  19747  taylply  19748  dvtaylp  19749  dvntaylp  19750  taylthlem1  19752  ulmdvlem1  19777  ulmdvlem3  19779  ulmdv  19780  dvsconst  26959  dvsid  26960  dvsef  26961  dvconstbi  26963  expgrowth  26964
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-resscn 8794
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-in 3159  df-ss 3166  df-sn 3646  df-pr 3647
  Copyright terms: Public domain W3C validator