Theorem recnprss 25939

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 4649	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 11212	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 4009	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 258	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 4042	. . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
6	4, 5	jaoi 858	. 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
7	1, 6	syl 17	1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Syntax hints:   → wi 4   ∨ wo 848   = wceq 1540   ∈ wcel 2108   ⊆ wss 3951  {cpr 4628  ℂcc 11153  ℝcr 11154

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-resscn 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968  df-sn 4627  df-pr 4629

This theorem is referenced by:  dvres3  25948  dvres3a  25949  dvcnp  25954  dvnff  25959  dvnadd  25965  dvnres  25967  cpnord  25971  cpncn  25972  cpnres  25973  dvadd  25977  dvmul  25978  dvaddf  25979  dvmulf  25980  dvcmul  25981  dvcmulf  25982  dvco  25985  dvcof  25986  dvmptid  25995  dvmptc  25996  dvmptres2  26000  dvmptcmul  26002  dvmptfsum  26013  dvcnvlem  26014  dvcnv  26015  dvlip2  26034  taylfvallem1  26398  tayl0  26403  taylply2  26409  taylply2OLD  26410  taylply  26411  dvtaylp  26412  dvntaylp  26413  taylthlem1  26415  ulmdvlem1  26443  ulmdvlem3  26445  ulmdv  26446  dvsconst  44349  dvsid  44350  dvsef  44351  dvconstbi  44353  expgrowth  44354  dvdmsscn  45951  dvnmptdivc  45953  dvnmptconst  45956  dvnxpaek  45957  dvnmul  45958  dvnprodlem3  45963