Theorem recnprss 26204

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 4608	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 11238	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 3956	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 261	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 3989	. . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
6	4, 5	jaoi 871	. 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
7	1, 6	syl 18	1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1570   ∈ wcel 2145   ⊆ wss 3899  {cpr 4586  ℂcc 11179  ℝcr 11180

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-resscn 11238

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-sn 4585  df-pr 4587

This theorem is used by:  dvres3  26213  dvres3a  26214  dvcnp  26219  dvnff  26223  dvnadd  26229  dvnres  26231  cpnord  26235  cpncn  26236  cpnres  26237  dvadd  26240  dvmul  26241  dvaddf  26242  dvmulf  26243  dvcmul  26244  dvcmulf  26245  dvco  26247  dvcof  26248  dvmptid  26257  dvmptc  26258  dvmptres2  26262  dvmptcmul  26264  dvmptfsum  26275  dvcnvlem  26276  dvcnv  26277  dvlip2  26295  taylfvallem1  26666  tayl0  26671  taylply2  26677  taylply  26678  dvtaylp  26679  dvntaylp  26680  taylthlem1  26682  ulmdvlem1  26709  ulmdvlem3  26711  ulmdv  26712  dvsconst  45273  dvsid  45274  dvsef  45275  dvconstbi  45277  expgrowth  45278  dvdmsscn  46890  dvnmptdivc  46892  dvnmptconst  46895  dvnxpaek  46896  dvnmul  46897  dvnprodlem3  46902