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

Theorem recnprss 25939
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 4649 . 2 (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2 ax-resscn 11212 . . . 4 ℝ ⊆ ℂ
3 sseq1 4009 . . . 4 (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
42, 3mpbiri 258 . . 3 (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5 eqimss 4042 . . 3 (𝑆 = ℂ → 𝑆 ⊆ ℂ)
64, 5jaoi 858 . 2 ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
71, 6syl 17 1 (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 848   = wceq 1540  wcel 2108  wss 3951  {cpr 4628  cc 11153  cr 11154
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-resscn 11212
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968  df-sn 4627  df-pr 4629
This theorem is referenced by:  dvres3  25948  dvres3a  25949  dvcnp  25954  dvnff  25959  dvnadd  25965  dvnres  25967  cpnord  25971  cpncn  25972  cpnres  25973  dvadd  25977  dvmul  25978  dvaddf  25979  dvmulf  25980  dvcmul  25981  dvcmulf  25982  dvco  25985  dvcof  25986  dvmptid  25995  dvmptc  25996  dvmptres2  26000  dvmptcmul  26002  dvmptfsum  26013  dvcnvlem  26014  dvcnv  26015  dvlip2  26034  taylfvallem1  26398  tayl0  26403  taylply2  26409  taylply2OLD  26410  taylply  26411  dvtaylp  26412  dvntaylp  26413  taylthlem1  26415  ulmdvlem1  26443  ulmdvlem3  26445  ulmdv  26446  dvsconst  44349  dvsid  44350  dvsef  44351  dvconstbi  44353  expgrowth  44354  dvdmsscn  45951  dvnmptdivc  45953  dvnmptconst  45956  dvnxpaek  45957  dvnmul  45958  dvnprodlem3  45963
  Copyright terms: Public domain W3C validator