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

Theorem recnprss 22602
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 3994 . 2  |-  ( S  e.  { RR ,  CC }  ->  ( S  =  RR  \/  S  =  CC ) )
2 ax-resscn 9581 . . . 4  |-  RR  C_  CC
3 sseq1 3465 . . . 4  |-  ( S  =  RR  ->  ( S  C_  CC  <->  RR  C_  CC ) )
42, 3mpbiri 235 . . 3  |-  ( S  =  RR  ->  S  C_  CC )
5 eqimss 3496 . . 3  |-  ( S  =  CC  ->  S  C_  CC )
64, 5jaoi 379 . 2  |-  ( ( S  =  RR  \/  S  =  CC )  ->  S  C_  CC )
71, 6syl 17 1  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 368    = wceq 1407    e. wcel 1844    C_ wss 3416   {cpr 3976   CCcc 9522   RRcr 9523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-resscn 9581
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-v 3063  df-un 3421  df-in 3423  df-ss 3430  df-sn 3975  df-pr 3977
This theorem is referenced by:  dvres3  22611  dvres3a  22612  dvcnp  22616  dvnff  22620  dvnadd  22626  dvnres  22628  cpnord  22632  cpncn  22633  cpnres  22634  dvadd  22637  dvmul  22638  dvaddf  22639  dvmulf  22640  dvcmul  22641  dvcmulf  22642  dvco  22644  dvcof  22645  dvmptid  22654  dvmptc  22655  dvmptres2  22659  dvmptcmul  22661  dvmptfsum  22670  dvcnvlem  22671  dvcnv  22672  dvlip2  22690  taylfvallem1  23046  tayl0  23051  taylply2  23057  taylply  23058  dvtaylp  23059  dvntaylp  23060  taylthlem1  23062  ulmdvlem1  23089  ulmdvlem3  23091  ulmdv  23092  dvsconst  36096  dvsid  36097  dvsef  36098  dvconstbi  36100  expgrowth  36101  dvdmsscn  37114  dvnmptdivc  37116  dvnmptconst  37119  dvnxpaek  37120  dvnmul  37121  dvnprodlem3  37126
  Copyright terms: Public domain W3C validator