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

Theorem recnprss 23888
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 4343 . 2 (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2 ax-resscn 10206 . . . 4 ℝ ⊆ ℂ
3 sseq1 3768 . . . 4 (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
42, 3mpbiri 248 . . 3 (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5 eqimss 3799 . . 3 (𝑆 = ℂ → 𝑆 ⊆ ℂ)
64, 5jaoi 393 . 2 ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
71, 6syl 17 1 (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382   = wceq 1632  wcel 2140  wss 3716  {cpr 4324  cc 10147  cr 10148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-resscn 10206
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-v 3343  df-un 3721  df-in 3723  df-ss 3730  df-sn 4323  df-pr 4325
This theorem is referenced by:  dvres3  23897  dvres3a  23898  dvcnp  23902  dvnff  23906  dvnadd  23912  dvnres  23914  cpnord  23918  cpncn  23919  cpnres  23920  dvadd  23923  dvmul  23924  dvaddf  23925  dvmulf  23926  dvcmul  23927  dvcmulf  23928  dvco  23930  dvcof  23931  dvmptid  23940  dvmptc  23941  dvmptres2  23945  dvmptcmul  23947  dvmptfsum  23958  dvcnvlem  23959  dvcnv  23960  dvlip2  23978  taylfvallem1  24331  tayl0  24336  taylply2  24342  taylply  24343  dvtaylp  24344  dvntaylp  24345  taylthlem1  24347  ulmdvlem1  24374  ulmdvlem3  24376  ulmdv  24377  dvsconst  39050  dvsid  39051  dvsef  39052  dvconstbi  39054  expgrowth  39055  dvdmsscn  40673  dvnmptdivc  40675  dvnmptconst  40678  dvnxpaek  40679  dvnmul  40680  dvnprodlem3  40685
  Copyright terms: Public domain W3C validator