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

Theorem recnprss 24501
Description: Both and are subsets of . (Contributed by Mario Carneiro, 10-Feb-2015.)
Assertion
Ref Expression
recnprss (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Proof of Theorem recnprss
StepHypRef Expression
1 elpri 4588 . 2 (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2 ax-resscn 10593 . . . 4 ℝ ⊆ ℂ
3 sseq1 3991 . . . 4 (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
42, 3mpbiri 260 . . 3 (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5 eqimss 4022 . . 3 (𝑆 = ℂ → 𝑆 ⊆ ℂ)
64, 5jaoi 853 . 2 ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
71, 6syl 17 1 (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 843   = wceq 1533  wcel 2110  wss 3935  {cpr 4568  cc 10534  cr 10535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-resscn 10593
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3940  df-in 3942  df-ss 3951  df-sn 4567  df-pr 4569
This theorem is referenced by:  dvres3  24510  dvres3a  24511  dvcnp  24515  dvnff  24519  dvnadd  24525  dvnres  24527  cpnord  24531  cpncn  24532  cpnres  24533  dvadd  24536  dvmul  24537  dvaddf  24538  dvmulf  24539  dvcmul  24540  dvcmulf  24541  dvco  24543  dvcof  24544  dvmptid  24553  dvmptc  24554  dvmptres2  24558  dvmptcmul  24560  dvmptfsum  24571  dvcnvlem  24572  dvcnv  24573  dvlip2  24591  taylfvallem1  24944  tayl0  24949  taylply2  24955  taylply  24956  dvtaylp  24957  dvntaylp  24958  taylthlem1  24960  ulmdvlem1  24987  ulmdvlem3  24989  ulmdv  24990  dvsconst  40662  dvsid  40663  dvsef  40664  dvconstbi  40666  expgrowth  40667  dvdmsscn  42221  dvnmptdivc  42223  dvnmptconst  42226  dvnxpaek  42227  dvnmul  42228  dvnprodlem3  42233
  Copyright terms: Public domain W3C validator