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

Theorem recnprss 23574
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 4168 . 2 (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2 ax-resscn 9937 . . . 4 ℝ ⊆ ℂ
3 sseq1 3605 . . . 4 (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
42, 3mpbiri 248 . . 3 (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5 eqimss 3636 . . 3 (𝑆 = ℂ → 𝑆 ⊆ ℂ)
64, 5jaoi 394 . 2 ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
71, 6syl 17 1 (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 383   = wceq 1480  wcel 1987  wss 3555  {cpr 4150  cc 9878  cr 9879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-resscn 9937
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-un 3560  df-in 3562  df-ss 3569  df-sn 4149  df-pr 4151
This theorem is referenced by:  dvres3  23583  dvres3a  23584  dvcnp  23588  dvnff  23592  dvnadd  23598  dvnres  23600  cpnord  23604  cpncn  23605  cpnres  23606  dvadd  23609  dvmul  23610  dvaddf  23611  dvmulf  23612  dvcmul  23613  dvcmulf  23614  dvco  23616  dvcof  23617  dvmptid  23626  dvmptc  23627  dvmptres2  23631  dvmptcmul  23633  dvmptfsum  23642  dvcnvlem  23643  dvcnv  23644  dvlip2  23662  taylfvallem1  24015  tayl0  24020  taylply2  24026  taylply  24027  dvtaylp  24028  dvntaylp  24029  taylthlem1  24031  ulmdvlem1  24058  ulmdvlem3  24060  ulmdv  24061  dvsconst  38008  dvsid  38009  dvsef  38010  dvconstbi  38012  expgrowth  38013  dvdmsscn  39454  dvnmptdivc  39456  dvnmptconst  39459  dvnxpaek  39460  dvnmul  39461  dvnprodlem3  39466
  Copyright terms: Public domain W3C validator