Theorem recnprss 25946

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 4605	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 11127	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 3961	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 260	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 3994	. . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
6	4, 5	jaoi 868	. 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
7	1, 6	syl 17	1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Syntax hints:   → wi 4   ∨ wo 858   = wceq 1559   ∈ wcel 2141   ⊆ wss 3904  {cpr 4583  ℂcc 11068  ℝcr 11069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-resscn 11127

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-ss 3921  df-sn 4582  df-pr 4584

This theorem is referenced by:  dvres3  25955  dvres3a  25956  dvcnp  25961  dvnff  25965  dvnadd  25971  dvnres  25973  cpnord  25977  cpncn  25978  cpnres  25979  dvadd  25982  dvmul  25983  dvaddf  25984  dvmulf  25985  dvcmul  25986  dvcmulf  25987  dvco  25989  dvcof  25990  dvmptid  25999  dvmptc  26000  dvmptres2  26004  dvmptcmul  26006  dvmptfsum  26017  dvcnvlem  26018  dvcnv  26019  dvlip2  26037  taylfvallem1  26397  tayl0  26402  taylply2  26408  taylply  26409  dvtaylp  26410  dvntaylp  26411  taylthlem1  26413  ulmdvlem1  26440  ulmdvlem3  26442  ulmdv  26443  dvsconst  44870  dvsid  44871  dvsef  44872  dvconstbi  44874  expgrowth  44875  dvdmsscn  46474  dvnmptdivc  46476  dvnmptconst  46479  dvnxpaek  46480  dvnmul  46481  dvnprodlem3  46486