Theorem recnprss 25428

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 4650	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 11169	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 4007	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 257	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 4040	. . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
6	4, 5	jaoi 855	. 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
7	1, 6	syl 17	1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Syntax hints:   → wi 4   ∨ wo 845   = wceq 1541   ∈ wcel 2106   ⊆ wss 3948  {cpr 4630  ℂcc 11110  ℝcr 11111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-resscn 11169

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953  df-in 3955  df-ss 3965  df-sn 4629  df-pr 4631

This theorem is referenced by:  dvres3  25437  dvres3a  25438  dvcnp  25443  dvnff  25447  dvnadd  25453  dvnres  25455  cpnord  25459  cpncn  25460  cpnres  25461  dvadd  25464  dvmul  25465  dvaddf  25466  dvmulf  25467  dvcmul  25468  dvcmulf  25469  dvco  25471  dvcof  25472  dvmptid  25481  dvmptc  25482  dvmptres2  25486  dvmptcmul  25488  dvmptfsum  25499  dvcnvlem  25500  dvcnv  25501  dvlip2  25519  taylfvallem1  25876  tayl0  25881  taylply2  25887  taylply  25888  dvtaylp  25889  dvntaylp  25890  taylthlem1  25892  ulmdvlem1  25919  ulmdvlem3  25921  ulmdv  25922  dvsconst  43171  dvsid  43172  dvsef  43173  dvconstbi  43175  expgrowth  43176  dvdmsscn  44731  dvnmptdivc  44733  dvnmptconst  44736  dvnxpaek  44737  dvnmul  44738  dvnprodlem3  44743