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

Theorem recnprss 23859
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 4334 . 2 (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2 ax-resscn 10177 . . . 4 ℝ ⊆ ℂ
3 sseq1 3759 . . . 4 (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
42, 3mpbiri 248 . . 3 (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5 eqimss 3790 . . 3 (𝑆 = ℂ → 𝑆 ⊆ ℂ)
64, 5jaoi 393 . 2 ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
71, 6syl 17 1 (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382   = wceq 1624  wcel 2131  wss 3707  {cpr 4315  cc 10118  cr 10119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-resscn 10177
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-v 3334  df-un 3712  df-in 3714  df-ss 3721  df-sn 4314  df-pr 4316
This theorem is referenced by:  dvres3  23868  dvres3a  23869  dvcnp  23873  dvnff  23877  dvnadd  23883  dvnres  23885  cpnord  23889  cpncn  23890  cpnres  23891  dvadd  23894  dvmul  23895  dvaddf  23896  dvmulf  23897  dvcmul  23898  dvcmulf  23899  dvco  23901  dvcof  23902  dvmptid  23911  dvmptc  23912  dvmptres2  23916  dvmptcmul  23918  dvmptfsum  23929  dvcnvlem  23930  dvcnv  23931  dvlip2  23949  taylfvallem1  24302  tayl0  24307  taylply2  24313  taylply  24314  dvtaylp  24315  dvntaylp  24316  taylthlem1  24318  ulmdvlem1  24345  ulmdvlem3  24347  ulmdv  24348  dvsconst  39023  dvsid  39024  dvsef  39025  dvconstbi  39027  expgrowth  39028  dvdmsscn  40646  dvnmptdivc  40648  dvnmptconst  40651  dvnxpaek  40652  dvnmul  40653  dvnprodlem3  40658
  Copyright terms: Public domain W3C validator