Theorem recnprss 25057

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 4585	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 10917	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 3947	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 257	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 3978	. . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
6	4, 5	jaoi 854	. 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
7	1, 6	syl 17	1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Syntax hints:   → wi 4   ∨ wo 844   = wceq 1539   ∈ wcel 2106   ⊆ wss 3888  {cpr 4565  ℂcc 10858  ℝcr 10859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-resscn 10917

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3433  df-un 3893  df-in 3895  df-ss 3905  df-sn 4564  df-pr 4566

This theorem is referenced by:  dvres3  25066  dvres3a  25067  dvcnp  25072  dvnff  25076  dvnadd  25082  dvnres  25084  cpnord  25088  cpncn  25089  cpnres  25090  dvadd  25093  dvmul  25094  dvaddf  25095  dvmulf  25096  dvcmul  25097  dvcmulf  25098  dvco  25100  dvcof  25101  dvmptid  25110  dvmptc  25111  dvmptres2  25115  dvmptcmul  25117  dvmptfsum  25128  dvcnvlem  25129  dvcnv  25130  dvlip2  25148  taylfvallem1  25505  tayl0  25510  taylply2  25516  taylply  25517  dvtaylp  25518  dvntaylp  25519  taylthlem1  25521  ulmdvlem1  25548  ulmdvlem3  25550  ulmdv  25551  dvsconst  41908  dvsid  41909  dvsef  41910  dvconstbi  41912  expgrowth  41913  dvdmsscn  43437  dvnmptdivc  43439  dvnmptconst  43442  dvnxpaek  43443  dvnmul  43444  dvnprodlem3  43449