Theorem recnprss 26044

Description: Both ℝ and ℂ are subsets of ℂ. (Contributed by Mario Carneiro, 10-Feb-2015.)

Assertion

Ref	Expression
recnprss	⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Proof of Theorem recnprss

Step	Hyp	Ref	Expression
1		elpri 4614	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 11158	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 3963	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 261	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 3996	. . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
6	4, 5	jaoi 870	. 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
7	1, 6	syl 18	1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Syntax hints:   → wi 4   ∨ wo 860   = wceq 1570   ∈ wcel 2143   ⊆ wss 3906  {cpr 4592  ℂcc 11099  ℝcr 11100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-resscn 11158

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-ss 3923  df-sn 4591  df-pr 4593

This theorem is referenced by:  dvres3  26053  dvres3a  26054  dvcnp  26059  dvnff  26063  dvnadd  26069  dvnres  26071  cpnord  26075  cpncn  26076  cpnres  26077  dvadd  26080  dvmul  26081  dvaddf  26082  dvmulf  26083  dvcmul  26084  dvcmulf  26085  dvco  26087  dvcof  26088  dvmptid  26097  dvmptc  26098  dvmptres2  26102  dvmptcmul  26104  dvmptfsum  26115  dvcnvlem  26116  dvcnv  26117  dvlip2  26135  taylfvallem1  26498  tayl0  26503  taylply2  26509  taylply  26510  dvtaylp  26511  dvntaylp  26512  taylthlem1  26514  ulmdvlem1  26541  ulmdvlem3  26543  ulmdv  26544  dvsconst  45020  dvsid  45021  dvsef  45022  dvconstbi  45024  expgrowth  45025  dvdmsscn  46630  dvnmptdivc  46632  dvnmptconst  46635  dvnxpaek  46636  dvnmul  46637  dvnprodlem3  46642