Theorem recnprss 25959

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

Syntax hints:   → wi 4   ∨ wo 846   = wceq 1537   ∈ wcel 2108   ⊆ wss 3976  {cpr 4650  ℂcc 11182  ℝcr 11183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-sn 4649  df-pr 4651

This theorem is referenced by:  dvres3  25968  dvres3a  25969  dvcnp  25974  dvnff  25979  dvnadd  25985  dvnres  25987  cpnord  25991  cpncn  25992  cpnres  25993  dvadd  25997  dvmul  25998  dvaddf  25999  dvmulf  26000  dvcmul  26001  dvcmulf  26002  dvco  26005  dvcof  26006  dvmptid  26015  dvmptc  26016  dvmptres2  26020  dvmptcmul  26022  dvmptfsum  26033  dvcnvlem  26034  dvcnv  26035  dvlip2  26054  taylfvallem1  26416  tayl0  26421  taylply2  26427  taylply2OLD  26428  taylply  26429  dvtaylp  26430  dvntaylp  26431  taylthlem1  26433  ulmdvlem1  26461  ulmdvlem3  26463  ulmdv  26464  dvsconst  44299  dvsid  44300  dvsef  44301  dvconstbi  44303  expgrowth  44304  dvdmsscn  45857  dvnmptdivc  45859  dvnmptconst  45862  dvnxpaek  45863  dvnmul  45864  dvnprodlem3  45869