Theorem recnprss 25861

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 4604	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 11083	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 3959	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 258	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 3992	. . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
6	4, 5	jaoi 857	. 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
7	1, 6	syl 17	1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1541   ∈ wcel 2113   ⊆ wss 3901  {cpr 4582  ℂcc 11024  ℝcr 11025

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-resscn 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-sn 4581  df-pr 4583

This theorem is referenced by:  dvres3  25870  dvres3a  25871  dvcnp  25876  dvnff  25881  dvnadd  25887  dvnres  25889  cpnord  25893  cpncn  25894  cpnres  25895  dvadd  25899  dvmul  25900  dvaddf  25901  dvmulf  25902  dvcmul  25903  dvcmulf  25904  dvco  25907  dvcof  25908  dvmptid  25917  dvmptc  25918  dvmptres2  25922  dvmptcmul  25924  dvmptfsum  25935  dvcnvlem  25936  dvcnv  25937  dvlip2  25956  taylfvallem1  26320  tayl0  26325  taylply2  26331  taylply2OLD  26332  taylply  26333  dvtaylp  26334  dvntaylp  26335  taylthlem1  26337  ulmdvlem1  26365  ulmdvlem3  26367  ulmdv  26368  dvsconst  44567  dvsid  44568  dvsef  44569  dvconstbi  44571  expgrowth  44572  dvdmsscn  46176  dvnmptdivc  46178  dvnmptconst  46181  dvnxpaek  46182  dvnmul  46183  dvnprodlem3  46188