Theorem recnprss 25826

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 4646	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 11189	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 4003	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 258	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 4036	. . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
6	4, 5	jaoi 856	. 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
7	1, 6	syl 17	1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Syntax hints:   → wi 4   ∨ wo 846   = wceq 1534   ∈ wcel 2099   ⊆ wss 3944  {cpr 4626  ℂcc 11130  ℝcr 11131

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-resscn 11189

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-un 3949  df-in 3951  df-ss 3961  df-sn 4625  df-pr 4627

This theorem is referenced by:  dvres3  25835  dvres3a  25836  dvcnp  25841  dvnff  25846  dvnadd  25852  dvnres  25854  cpnord  25858  cpncn  25859  cpnres  25860  dvadd  25864  dvmul  25865  dvaddf  25866  dvmulf  25867  dvcmul  25868  dvcmulf  25869  dvco  25872  dvcof  25873  dvmptid  25882  dvmptc  25883  dvmptres2  25887  dvmptcmul  25889  dvmptfsum  25900  dvcnvlem  25901  dvcnv  25902  dvlip2  25921  taylfvallem1  26284  tayl0  26289  taylply2  26295  taylply2OLD  26296  taylply  26297  dvtaylp  26298  dvntaylp  26299  taylthlem1  26301  ulmdvlem1  26329  ulmdvlem3  26331  ulmdv  26332  dvsconst  43739  dvsid  43740  dvsef  43741  dvconstbi  43743  expgrowth  43744  dvdmsscn  45296  dvnmptdivc  45298  dvnmptconst  45301  dvnxpaek  45302  dvnmul  45303  dvnprodlem3  45308