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

Theorem recnprss 19783
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 3826 . 2  |-  ( S  e.  { RR ,  CC }  ->  ( S  =  RR  \/  S  =  CC ) )
2 ax-resscn 9039 . . . 4  |-  RR  C_  CC
3 sseq1 3361 . . . 4  |-  ( S  =  RR  ->  ( S  C_  CC  <->  RR  C_  CC ) )
42, 3mpbiri 225 . . 3  |-  ( S  =  RR  ->  S  C_  CC )
5 eqimss 3392 . . 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 1652    e. wcel 1725    C_ wss 3312   {cpr 3807   CCcc 8980   RRcr 8981
This theorem is referenced by:  dvres3  19792  dvres3a  19793  dvcnp  19797  dvnff  19801  dvnadd  19807  dvnres  19809  cpnord  19813  cpncn  19814  cpnres  19815  dvadd  19818  dvmul  19819  dvaddf  19820  dvmulf  19821  dvcmul  19822  dvcmulf  19823  dvco  19825  dvcof  19826  dvmptid  19835  dvmptc  19836  dvmptres2  19840  dvmptcmul  19842  dvmptfsum  19851  dvcnvlem  19852  dvcnv  19853  dvlip2  19871  taylfvallem1  20265  tayl0  20270  taylply2  20276  taylply  20277  dvtaylp  20278  dvntaylp  20279  taylthlem1  20281  ulmdvlem1  20308  ulmdvlem3  20310  ulmdv  20311  dvsconst  27515  dvsid  27516  dvsef  27517  dvconstbi  27519  expgrowth  27520
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-resscn 9039
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-un 3317  df-in 3319  df-ss 3326  df-sn 3812  df-pr 3813
  Copyright terms: Public domain W3C validator