Theorem recnprss 26257

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 11287	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 3938	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 261	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 3971	. . 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 2147   ⊆ wss 3900  {cpr 4590  ℂcc 11228  ℝcr 11229

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-resscn 11287

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  dvres3  26266  dvres3a  26267  dvcnp  26272  dvnff  26276  dvnadd  26282  dvnres  26284  cpnord  26288  cpncn  26289  cpnres  26290  dvadd  26293  dvmul  26294  dvaddf  26295  dvmulf  26296  dvcmul  26297  dvcmulf  26298  dvco  26300  dvcof  26301  dvmptid  26310  dvmptc  26311  dvmptres2  26315  dvmptcmul  26317  dvmptfsum  26328  dvcnvlem  26329  dvcnv  26330  dvlip2  26348  taylfvallem1  26717  tayl0  26722  taylply2  26728  taylply  26729  dvtaylp  26730  dvntaylp  26731  taylthlem1  26733  ulmdvlem1  26760  ulmdvlem3  26762  ulmdv  26763  dvsconst  45517  dvsid  45518  dvsef  45519  dvconstbi  45521  expgrowth  45522  dvdmsscn  47161  dvnmptdivc  47163  dvnmptconst  47166  dvnxpaek  47167  dvnmul  47168  dvnprodlem3  47173