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

Theorem recnprss 19658
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 3777 . 2  |-  ( S  e.  { RR ,  CC }  ->  ( S  =  RR  \/  S  =  CC ) )
2 ax-resscn 8980 . . . 4  |-  RR  C_  CC
3 sseq1 3312 . . . 4  |-  ( S  =  RR  ->  ( S  C_  CC  <->  RR  C_  CC ) )
42, 3mpbiri 225 . . 3  |-  ( S  =  RR  ->  S  C_  CC )
5 eqimss 3343 . . 3  |-  ( S  =  CC  ->  S  C_  CC )
64, 5jaoi 369 . 2  |-  ( ( S  =  RR  \/  S  =  CC )  ->  S  C_  CC )
71, 6syl 16 1  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358    = wceq 1649    e. wcel 1717    C_ wss 3263   {cpr 3758   CCcc 8921   RRcr 8922
This theorem is referenced by:  dvres3  19667  dvres3a  19668  dvcnp  19672  dvnff  19676  dvnadd  19682  dvnres  19684  cpnord  19688  cpncn  19689  cpnres  19690  dvadd  19693  dvmul  19694  dvaddf  19695  dvmulf  19696  dvcmul  19697  dvcmulf  19698  dvco  19700  dvcof  19701  dvmptid  19710  dvmptc  19711  dvmptres2  19715  dvmptcmul  19717  dvmptfsum  19726  dvcnvlem  19727  dvcnv  19728  dvlip2  19746  taylfvallem1  20140  tayl0  20145  taylply2  20151  taylply  20152  dvtaylp  20153  dvntaylp  20154  taylthlem1  20156  ulmdvlem1  20183  ulmdvlem3  20185  ulmdv  20186  dvsconst  27216  dvsid  27217  dvsef  27218  dvconstbi  27220  expgrowth  27221
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-resscn 8980
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901  df-un 3268  df-in 3270  df-ss 3277  df-sn 3763  df-pr 3764
  Copyright terms: Public domain W3C validator