Theorem recnprss 25953

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1536   ∈ wcel 2105   ⊆ wss 3962  {cpr 4632  ℂcc 11150  ℝcr 11151

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-resscn 11209

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-ss 3979  df-sn 4631  df-pr 4633

This theorem is referenced by:  dvres3  25962  dvres3a  25963  dvcnp  25968  dvnff  25973  dvnadd  25979  dvnres  25981  cpnord  25985  cpncn  25986  cpnres  25987  dvadd  25991  dvmul  25992  dvaddf  25993  dvmulf  25994  dvcmul  25995  dvcmulf  25996  dvco  25999  dvcof  26000  dvmptid  26009  dvmptc  26010  dvmptres2  26014  dvmptcmul  26016  dvmptfsum  26027  dvcnvlem  26028  dvcnv  26029  dvlip2  26048  taylfvallem1  26412  tayl0  26417  taylply2  26423  taylply2OLD  26424  taylply  26425  dvtaylp  26426  dvntaylp  26427  taylthlem1  26429  ulmdvlem1  26457  ulmdvlem3  26459  ulmdv  26460  dvsconst  44325  dvsid  44326  dvsef  44327  dvconstbi  44329  expgrowth  44330  dvdmsscn  45891  dvnmptdivc  45893  dvnmptconst  45896  dvnxpaek  45897  dvnmul  45898  dvnprodlem3  45903