Theorem recnprss 25833

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1541   ∈ wcel 2113   ⊆ wss 3898  {cpr 4577  ℂcc 11011  ℝcr 11012

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 2705  ax-resscn 11070

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 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-ss 3915  df-sn 4576  df-pr 4578

This theorem is referenced by:  dvres3  25842  dvres3a  25843  dvcnp  25848  dvnff  25853  dvnadd  25859  dvnres  25861  cpnord  25865  cpncn  25866  cpnres  25867  dvadd  25871  dvmul  25872  dvaddf  25873  dvmulf  25874  dvcmul  25875  dvcmulf  25876  dvco  25879  dvcof  25880  dvmptid  25889  dvmptc  25890  dvmptres2  25894  dvmptcmul  25896  dvmptfsum  25907  dvcnvlem  25908  dvcnv  25909  dvlip2  25928  taylfvallem1  26292  tayl0  26297  taylply2  26303  taylply2OLD  26304  taylply  26305  dvtaylp  26306  dvntaylp  26307  taylthlem1  26309  ulmdvlem1  26337  ulmdvlem3  26339  ulmdv  26340  dvsconst  44447  dvsid  44448  dvsef  44449  dvconstbi  44451  expgrowth  44452  dvdmsscn  46058  dvnmptdivc  46060  dvnmptconst  46063  dvnxpaek  46064  dvnmul  46065  dvnprodlem3  46070