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

Theorem recnprss 25826
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 4646 . 2 (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2 ax-resscn 11189 . . . 4 ℝ ⊆ ℂ
3 sseq1 4003 . . . 4 (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
42, 3mpbiri 258 . . 3 (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5 eqimss 4036 . . 3 (𝑆 = ℂ → 𝑆 ⊆ ℂ)
64, 5jaoi 856 . 2 ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
71, 6syl 17 1 (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 846   = wceq 1534  wcel 2099  wss 3944  {cpr 4626  cc 11130  cr 11131
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-resscn 11189
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-un 3949  df-in 3951  df-ss 3961  df-sn 4625  df-pr 4627
This theorem is referenced by:  dvres3  25835  dvres3a  25836  dvcnp  25841  dvnff  25846  dvnadd  25852  dvnres  25854  cpnord  25858  cpncn  25859  cpnres  25860  dvadd  25864  dvmul  25865  dvaddf  25866  dvmulf  25867  dvcmul  25868  dvcmulf  25869  dvco  25872  dvcof  25873  dvmptid  25882  dvmptc  25883  dvmptres2  25887  dvmptcmul  25889  dvmptfsum  25900  dvcnvlem  25901  dvcnv  25902  dvlip2  25921  taylfvallem1  26284  tayl0  26289  taylply2  26295  taylply2OLD  26296  taylply  26297  dvtaylp  26298  dvntaylp  26299  taylthlem1  26301  ulmdvlem1  26329  ulmdvlem3  26331  ulmdv  26332  dvsconst  43739  dvsid  43740  dvsef  43741  dvconstbi  43743  expgrowth  43744  dvdmsscn  45296  dvnmptdivc  45298  dvnmptconst  45301  dvnxpaek  45302  dvnmul  45303  dvnprodlem3  45308
  Copyright terms: Public domain W3C validator