Theorem recnprss 24973

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 4580	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 10859	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 3942	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 257	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 3973	. . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
6	4, 5	jaoi 853	. 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
7	1, 6	syl 17	1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Syntax hints:   → wi 4   ∨ wo 843   = wceq 1539   ∈ wcel 2108   ⊆ wss 3883  {cpr 4560  ℂcc 10800  ℝcr 10801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-sn 4559  df-pr 4561

This theorem is referenced by:  dvres3  24982  dvres3a  24983  dvcnp  24988  dvnff  24992  dvnadd  24998  dvnres  25000  cpnord  25004  cpncn  25005  cpnres  25006  dvadd  25009  dvmul  25010  dvaddf  25011  dvmulf  25012  dvcmul  25013  dvcmulf  25014  dvco  25016  dvcof  25017  dvmptid  25026  dvmptc  25027  dvmptres2  25031  dvmptcmul  25033  dvmptfsum  25044  dvcnvlem  25045  dvcnv  25046  dvlip2  25064  taylfvallem1  25421  tayl0  25426  taylply2  25432  taylply  25433  dvtaylp  25434  dvntaylp  25435  taylthlem1  25437  ulmdvlem1  25464  ulmdvlem3  25466  ulmdv  25467  dvsconst  41837  dvsid  41838  dvsef  41839  dvconstbi  41841  expgrowth  41842  dvdmsscn  43367  dvnmptdivc  43369  dvnmptconst  43372  dvnxpaek  43373  dvnmul  43374  dvnprodlem3  43379