Theorem recnprss 25830

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1541   ∈ wcel 2111   ⊆ wss 3902  {cpr 4578  ℂcc 11001  ℝcr 11002

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 2113  ax-9 2121  ax-ext 2703  ax-resscn 11060

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-ss 3919  df-sn 4577  df-pr 4579

This theorem is referenced by:  dvres3  25839  dvres3a  25840  dvcnp  25845  dvnff  25850  dvnadd  25856  dvnres  25858  cpnord  25862  cpncn  25863  cpnres  25864  dvadd  25868  dvmul  25869  dvaddf  25870  dvmulf  25871  dvcmul  25872  dvcmulf  25873  dvco  25876  dvcof  25877  dvmptid  25886  dvmptc  25887  dvmptres2  25891  dvmptcmul  25893  dvmptfsum  25904  dvcnvlem  25905  dvcnv  25906  dvlip2  25925  taylfvallem1  26289  tayl0  26294  taylply2  26300  taylply2OLD  26301  taylply  26302  dvtaylp  26303  dvntaylp  26304  taylthlem1  26306  ulmdvlem1  26334  ulmdvlem3  26336  ulmdv  26337  dvsconst  44362  dvsid  44363  dvsef  44364  dvconstbi  44366  expgrowth  44367  dvdmsscn  45973  dvnmptdivc  45975  dvnmptconst  45978  dvnxpaek  45979  dvnmul  45980  dvnprodlem3  45985