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

Theorem recnprss 22043
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 4047 . 2  |-  ( S  e.  { RR ,  CC }  ->  ( S  =  RR  \/  S  =  CC ) )
2 ax-resscn 9545 . . . 4  |-  RR  C_  CC
3 sseq1 3525 . . . 4  |-  ( S  =  RR  ->  ( S  C_  CC  <->  RR  C_  CC ) )
42, 3mpbiri 233 . . 3  |-  ( S  =  RR  ->  S  C_  CC )
5 eqimss 3556 . . 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 1379    e. wcel 1767    C_ wss 3476   {cpr 4029   CCcc 9486   RRcr 9487
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-resscn 9545
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-in 3483  df-ss 3490  df-sn 4028  df-pr 4030
This theorem is referenced by:  dvres3  22052  dvres3a  22053  dvcnp  22057  dvnff  22061  dvnadd  22067  dvnres  22069  cpnord  22073  cpncn  22074  cpnres  22075  dvadd  22078  dvmul  22079  dvaddf  22080  dvmulf  22081  dvcmul  22082  dvcmulf  22083  dvco  22085  dvcof  22086  dvmptid  22095  dvmptc  22096  dvmptres2  22100  dvmptcmul  22102  dvmptfsum  22111  dvcnvlem  22112  dvcnv  22113  dvlip2  22131  taylfvallem1  22486  tayl0  22491  taylply2  22497  taylply  22498  dvtaylp  22499  dvntaylp  22500  taylthlem1  22502  ulmdvlem1  22529  ulmdvlem3  22531  ulmdv  22532  dvsconst  30835  dvsid  30836  dvsef  30837  dvconstbi  30839  expgrowth  30840
  Copyright terms: Public domain W3C validator