Theorem recnprss 25896

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 4586	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 11093	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 3947	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 259	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 3980	. . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
6	4, 5	jaoi 863	. 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
7	1, 6	syl 17	1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Syntax hints:   → wi 4   ∨ wo 853   = wceq 1547   ∈ wcel 2119   ⊆ wss 3890  {cpr 4564  ℂcc 11034  ℝcr 11035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-resscn 11093

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-ss 3907  df-sn 4563  df-pr 4565

This theorem is referenced by:  dvres3  25905  dvres3a  25906  dvcnp  25911  dvnff  25915  dvnadd  25921  dvnres  25923  cpnord  25927  cpncn  25928  cpnres  25929  dvadd  25932  dvmul  25933  dvaddf  25934  dvmulf  25935  dvcmul  25936  dvcmulf  25937  dvco  25939  dvcof  25940  dvmptid  25949  dvmptc  25950  dvmptres2  25954  dvmptcmul  25956  dvmptfsum  25967  dvcnvlem  25968  dvcnv  25969  dvlip2  25987  taylfvallem1  26347  tayl0  26352  taylply2  26358  taylply  26359  dvtaylp  26360  dvntaylp  26361  taylthlem1  26363  ulmdvlem1  26390  ulmdvlem3  26392  ulmdv  26393  dvsconst  44781  dvsid  44782  dvsef  44783  dvconstbi  44785  expgrowth  44786  dvdmsscn  46386  dvnmptdivc  46388  dvnmptconst  46391  dvnxpaek  46392  dvnmul  46393  dvnprodlem3  46398