Theorem recnprss 26028

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

Syntax hints:   → wi 4   ∨ wo 860   = wceq 1567   ∈ wcel 2149   ⊆ wss 3913  {cpr 4593  ℂcc 11094  ℝcr 11095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-resscn 11153

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930  df-sn 4592  df-pr 4594

This theorem is referenced by:  dvres3  26037  dvres3a  26038  dvcnp  26043  dvnff  26047  dvnadd  26053  dvnres  26055  cpnord  26059  cpncn  26060  cpnres  26061  dvadd  26064  dvmul  26065  dvaddf  26066  dvmulf  26067  dvcmul  26068  dvcmulf  26069  dvco  26071  dvcof  26072  dvmptid  26081  dvmptc  26082  dvmptres2  26086  dvmptcmul  26088  dvmptfsum  26099  dvcnvlem  26100  dvcnv  26101  dvlip2  26119  taylfvallem1  26482  tayl0  26487  taylply2  26493  taylply  26494  dvtaylp  26495  dvntaylp  26496  taylthlem1  26498  ulmdvlem1  26525  ulmdvlem3  26527  ulmdv  26528  dvsconst  44927  dvsid  44928  dvsef  44929  dvconstbi  44931  expgrowth  44932  dvdmsscn  46537  dvnmptdivc  46539  dvnmptconst  46542  dvnxpaek  46543  dvnmul  46544  dvnprodlem3  46549