Theorem recnprss 25812

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ⊆ wss 3917  {cpr 4594  ℂcc 11073  ℝcr 11074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-resscn 11132

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-sn 4593  df-pr 4595

This theorem is referenced by:  dvres3  25821  dvres3a  25822  dvcnp  25827  dvnff  25832  dvnadd  25838  dvnres  25840  cpnord  25844  cpncn  25845  cpnres  25846  dvadd  25850  dvmul  25851  dvaddf  25852  dvmulf  25853  dvcmul  25854  dvcmulf  25855  dvco  25858  dvcof  25859  dvmptid  25868  dvmptc  25869  dvmptres2  25873  dvmptcmul  25875  dvmptfsum  25886  dvcnvlem  25887  dvcnv  25888  dvlip2  25907  taylfvallem1  26271  tayl0  26276  taylply2  26282  taylply2OLD  26283  taylply  26284  dvtaylp  26285  dvntaylp  26286  taylthlem1  26288  ulmdvlem1  26316  ulmdvlem3  26318  ulmdv  26319  dvsconst  44326  dvsid  44327  dvsef  44328  dvconstbi  44330  expgrowth  44331  dvdmsscn  45941  dvnmptdivc  45943  dvnmptconst  45946  dvnxpaek  45947  dvnmul  45948  dvnprodlem3  45953