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

Theorem recnprss 21507
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 4000 . 2  |-  ( S  e.  { RR ,  CC }  ->  ( S  =  RR  \/  S  =  CC ) )
2 ax-resscn 9445 . . . 4  |-  RR  C_  CC
3 sseq1 3480 . . . 4  |-  ( S  =  RR  ->  ( S  C_  CC  <->  RR  C_  CC ) )
42, 3mpbiri 233 . . 3  |-  ( S  =  RR  ->  S  C_  CC )
5 eqimss 3511 . . 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 1370    e. wcel 1758    C_ wss 3431   {cpr 3982   CCcc 9386   RRcr 9387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431  ax-resscn 9445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-v 3074  df-un 3436  df-in 3438  df-ss 3445  df-sn 3981  df-pr 3983
This theorem is referenced by:  dvres3  21516  dvres3a  21517  dvcnp  21521  dvnff  21525  dvnadd  21531  dvnres  21533  cpnord  21537  cpncn  21538  cpnres  21539  dvadd  21542  dvmul  21543  dvaddf  21544  dvmulf  21545  dvcmul  21546  dvcmulf  21547  dvco  21549  dvcof  21550  dvmptid  21559  dvmptc  21560  dvmptres2  21564  dvmptcmul  21566  dvmptfsum  21575  dvcnvlem  21576  dvcnv  21577  dvlip2  21595  taylfvallem1  21950  tayl0  21955  taylply2  21961  taylply  21962  dvtaylp  21963  dvntaylp  21964  taylthlem1  21966  ulmdvlem1  21993  ulmdvlem3  21995  ulmdv  21996  dvsconst  29747  dvsid  29748  dvsef  29749  dvconstbi  29751  expgrowth  29752
  Copyright terms: Public domain W3C validator