Theorem recnprss 25821

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ⊆ wss 3905  {cpr 4581  ℂcc 11026  ℝcr 11027

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 2701  ax-resscn 11085

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 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-ss 3922  df-sn 4580  df-pr 4582

This theorem is referenced by:  dvres3  25830  dvres3a  25831  dvcnp  25836  dvnff  25841  dvnadd  25847  dvnres  25849  cpnord  25853  cpncn  25854  cpnres  25855  dvadd  25859  dvmul  25860  dvaddf  25861  dvmulf  25862  dvcmul  25863  dvcmulf  25864  dvco  25867  dvcof  25868  dvmptid  25877  dvmptc  25878  dvmptres2  25882  dvmptcmul  25884  dvmptfsum  25895  dvcnvlem  25896  dvcnv  25897  dvlip2  25916  taylfvallem1  26280  tayl0  26285  taylply2  26291  taylply2OLD  26292  taylply  26293  dvtaylp  26294  dvntaylp  26295  taylthlem1  26297  ulmdvlem1  26325  ulmdvlem3  26327  ulmdv  26328  dvsconst  44303  dvsid  44304  dvsef  44305  dvconstbi  44307  expgrowth  44308  dvdmsscn  45918  dvnmptdivc  45920  dvnmptconst  45923  dvnxpaek  45924  dvnmul  45925  dvnprodlem3  45930