Theorem recnprss 26024

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 4609	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 11145	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 3964	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 261	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 3997	. . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
6	4, 5	jaoi 870	. 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
7	1, 6	syl 18	1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Syntax hints:   → wi 4   ∨ wo 860   = wceq 1563   ∈ wcel 2145   ⊆ wss 3907  {cpr 4587  ℂcc 11086  ℝcr 11087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-resscn 11145

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924  df-sn 4586  df-pr 4588

This theorem is referenced by:  dvres3  26033  dvres3a  26034  dvcnp  26039  dvnff  26043  dvnadd  26049  dvnres  26051  cpnord  26055  cpncn  26056  cpnres  26057  dvadd  26060  dvmul  26061  dvaddf  26062  dvmulf  26063  dvcmul  26064  dvcmulf  26065  dvco  26067  dvcof  26068  dvmptid  26077  dvmptc  26078  dvmptres2  26082  dvmptcmul  26084  dvmptfsum  26095  dvcnvlem  26096  dvcnv  26097  dvlip2  26115  taylfvallem1  26478  tayl0  26483  taylply2  26489  taylply  26490  dvtaylp  26491  dvntaylp  26492  taylthlem1  26494  ulmdvlem1  26521  ulmdvlem3  26523  ulmdv  26524  dvsconst  44904  dvsid  44905  dvsef  44906  dvconstbi  44908  expgrowth  44909  dvdmsscn  46508  dvnmptdivc  46510  dvnmptconst  46513  dvnxpaek  46514  dvnmul  46515  dvnprodlem3  46520