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

Theorem recnprss 19796
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 3836 . 2  |-  ( S  e.  { RR ,  CC }  ->  ( S  =  RR  \/  S  =  CC ) )
2 ax-resscn 9052 . . . 4  |-  RR  C_  CC
3 sseq1 3371 . . . 4  |-  ( S  =  RR  ->  ( S  C_  CC  <->  RR  C_  CC ) )
42, 3mpbiri 226 . . 3  |-  ( S  =  RR  ->  S  C_  CC )
5 eqimss 3402 . . 3  |-  ( S  =  CC  ->  S  C_  CC )
64, 5jaoi 370 . 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 359    = wceq 1653    e. wcel 1726    C_ wss 3322   {cpr 3817   CCcc 8993   RRcr 8994
This theorem is referenced by:  dvres3  19805  dvres3a  19806  dvcnp  19810  dvnff  19814  dvnadd  19820  dvnres  19822  cpnord  19826  cpncn  19827  cpnres  19828  dvadd  19831  dvmul  19832  dvaddf  19833  dvmulf  19834  dvcmul  19835  dvcmulf  19836  dvco  19838  dvcof  19839  dvmptid  19848  dvmptc  19849  dvmptres2  19853  dvmptcmul  19855  dvmptfsum  19864  dvcnvlem  19865  dvcnv  19866  dvlip2  19884  taylfvallem1  20278  tayl0  20283  taylply2  20289  taylply  20290  dvtaylp  20291  dvntaylp  20292  taylthlem1  20294  ulmdvlem1  20321  ulmdvlem3  20323  ulmdv  20324  dvsconst  27538  dvsid  27539  dvsef  27540  dvconstbi  27542  expgrowth  27543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-resscn 9052
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-un 3327  df-in 3329  df-ss 3336  df-sn 3822  df-pr 3823
  Copyright terms: Public domain W3C validator