Theorem recnprss 26229

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1569   ∈ wcel 2144   ⊆ wss 3895  {cpr 4586  ℂcc 11201  ℝcr 11202

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-resscn 11260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151  df-sn 4585  df-pr 4587

This theorem is used by:  dvres3  26238  dvres3a  26239  dvcnp  26244  dvnff  26248  dvnadd  26254  dvnres  26256  cpnord  26260  cpncn  26261  cpnres  26262  dvadd  26265  dvmul  26266  dvaddf  26267  dvmulf  26268  dvcmul  26269  dvcmulf  26270  dvco  26272  dvcof  26273  dvmptid  26282  dvmptc  26283  dvmptres2  26287  dvmptcmul  26289  dvmptfsum  26300  dvcnvlem  26301  dvcnv  26302  dvlip2  26320  taylfvallem1  26689  tayl0  26694  taylply2  26700  taylply  26701  dvtaylp  26702  dvntaylp  26703  taylthlem1  26705  ulmdvlem1  26732  ulmdvlem3  26734  ulmdv  26735  dvsconst  45407  dvsid  45408  dvsef  45409  dvconstbi  45411  expgrowth  45412  dvdmsscn  47039  dvnmptdivc  47041  dvnmptconst  47044  dvnxpaek  47045  dvnmul  47046  dvnprodlem3  47051