Theorem recnprss 26100

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 4618	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 11175	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 3965	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 261	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 3998	. . 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 2146   ⊆ wss 3908  {cpr 4596  ℂcc 11116  ℝcr 11117

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 2148  ax-9 2156  ax-ext 2738  ax-resscn 11175

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 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-ss 3925  df-sn 4595  df-pr 4597

This theorem is used by:  dvres3  26109  dvres3a  26110  dvcnp  26115  dvnff  26119  dvnadd  26125  dvnres  26127  cpnord  26131  cpncn  26132  cpnres  26133  dvadd  26136  dvmul  26137  dvaddf  26138  dvmulf  26139  dvcmul  26140  dvcmulf  26141  dvco  26143  dvcof  26144  dvmptid  26153  dvmptc  26154  dvmptres2  26158  dvmptcmul  26160  dvmptfsum  26171  dvcnvlem  26172  dvcnv  26173  dvlip2  26191  taylfvallem1  26557  tayl0  26562  taylply2  26568  taylply  26569  dvtaylp  26570  dvntaylp  26571  taylthlem1  26573  ulmdvlem1  26600  ulmdvlem3  26602  ulmdv  26603  dvsconst  45081  dvsid  45082  dvsef  45083  dvconstbi  45085  expgrowth  45086  dvdmsscn  46691  dvnmptdivc  46693  dvnmptconst  46696  dvnxpaek  46697  dvnmul  46698  dvnprodlem3  46703