Theorem recnprss 25871

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

Syntax hints:   → wi 4   ∨ wo 848   = wceq 1542   ∈ wcel 2114   ⊆ wss 3889  {cpr 4569  ℂcc 11036  ℝcr 11037

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-sn 4568  df-pr 4570

This theorem is referenced by:  dvres3  25880  dvres3a  25881  dvcnp  25886  dvnff  25890  dvnadd  25896  dvnres  25898  cpnord  25902  cpncn  25903  cpnres  25904  dvadd  25907  dvmul  25908  dvaddf  25909  dvmulf  25910  dvcmul  25911  dvcmulf  25912  dvco  25914  dvcof  25915  dvmptid  25924  dvmptc  25925  dvmptres2  25929  dvmptcmul  25931  dvmptfsum  25942  dvcnvlem  25943  dvcnv  25944  dvlip2  25962  taylfvallem1  26322  tayl0  26327  taylply2  26333  taylply  26334  dvtaylp  26335  dvntaylp  26336  taylthlem1  26338  ulmdvlem1  26365  ulmdvlem3  26367  ulmdv  26368  dvsconst  44757  dvsid  44758  dvsef  44759  dvconstbi  44761  expgrowth  44762  dvdmsscn  46364  dvnmptdivc  46366  dvnmptconst  46369  dvnxpaek  46370  dvnmul  46371  dvnprodlem3  46376