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

Theorem recnprss 24105
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 4420 . 2 (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2 ax-resscn 10329 . . . 4 ℝ ⊆ ℂ
3 sseq1 3845 . . . 4 (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
42, 3mpbiri 250 . . 3 (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5 eqimss 3876 . . 3 (𝑆 = ℂ → 𝑆 ⊆ ℂ)
64, 5jaoi 846 . 2 ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
71, 6syl 17 1 (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 836   = wceq 1601  wcel 2107  wss 3792  {cpr 4400  cc 10270  cr 10271
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754  ax-resscn 10329
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-un 3797  df-in 3799  df-ss 3806  df-sn 4399  df-pr 4401
This theorem is referenced by:  dvres3  24114  dvres3a  24115  dvcnp  24119  dvnff  24123  dvnadd  24129  dvnres  24131  cpnord  24135  cpncn  24136  cpnres  24137  dvadd  24140  dvmul  24141  dvaddf  24142  dvmulf  24143  dvcmul  24144  dvcmulf  24145  dvco  24147  dvcof  24148  dvmptid  24157  dvmptc  24158  dvmptres2  24162  dvmptcmul  24164  dvmptfsum  24175  dvcnvlem  24176  dvcnv  24177  dvlip2  24195  taylfvallem1  24548  tayl0  24553  taylply2  24559  taylply  24560  dvtaylp  24561  dvntaylp  24562  taylthlem1  24564  ulmdvlem1  24591  ulmdvlem3  24593  ulmdv  24594  dvsconst  39485  dvsid  39486  dvsef  39487  dvconstbi  39489  expgrowth  39490  dvdmsscn  41079  dvnmptdivc  41081  dvnmptconst  41084  dvnxpaek  41085  dvnmul  41086  dvnprodlem3  41091
  Copyright terms: Public domain W3C validator