Theorem recnprss 25805

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 4613	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 11125	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 3972	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 258	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 4005	. . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
6	4, 5	jaoi 857	. 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
7	1, 6	syl 17	1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ⊆ wss 3914  {cpr 4591  ℂcc 11066  ℝcr 11067

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11125

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931  df-sn 4590  df-pr 4592

This theorem is referenced by:  dvres3  25814  dvres3a  25815  dvcnp  25820  dvnff  25825  dvnadd  25831  dvnres  25833  cpnord  25837  cpncn  25838  cpnres  25839  dvadd  25843  dvmul  25844  dvaddf  25845  dvmulf  25846  dvcmul  25847  dvcmulf  25848  dvco  25851  dvcof  25852  dvmptid  25861  dvmptc  25862  dvmptres2  25866  dvmptcmul  25868  dvmptfsum  25879  dvcnvlem  25880  dvcnv  25881  dvlip2  25900  taylfvallem1  26264  tayl0  26269  taylply2  26275  taylply2OLD  26276  taylply  26277  dvtaylp  26278  dvntaylp  26279  taylthlem1  26281  ulmdvlem1  26309  ulmdvlem3  26311  ulmdv  26312  dvsconst  44319  dvsid  44320  dvsef  44321  dvconstbi  44323  expgrowth  44324  dvdmsscn  45934  dvnmptdivc  45936  dvnmptconst  45939  dvnxpaek  45940  dvnmul  45941  dvnprodlem3  45946