Theorem recnprss 25857

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1540   ∈ wcel 2108   ⊆ wss 3926  {cpr 4603  ℂcc 11127  ℝcr 11128

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 2707  ax-resscn 11186

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943  df-sn 4602  df-pr 4604

This theorem is referenced by:  dvres3  25866  dvres3a  25867  dvcnp  25872  dvnff  25877  dvnadd  25883  dvnres  25885  cpnord  25889  cpncn  25890  cpnres  25891  dvadd  25895  dvmul  25896  dvaddf  25897  dvmulf  25898  dvcmul  25899  dvcmulf  25900  dvco  25903  dvcof  25904  dvmptid  25913  dvmptc  25914  dvmptres2  25918  dvmptcmul  25920  dvmptfsum  25931  dvcnvlem  25932  dvcnv  25933  dvlip2  25952  taylfvallem1  26316  tayl0  26321  taylply2  26327  taylply2OLD  26328  taylply  26329  dvtaylp  26330  dvntaylp  26331  taylthlem1  26333  ulmdvlem1  26361  ulmdvlem3  26363  ulmdv  26364  dvsconst  44354  dvsid  44355  dvsef  44356  dvconstbi  44358  expgrowth  44359  dvdmsscn  45965  dvnmptdivc  45967  dvnmptconst  45970  dvnxpaek  45971  dvnmul  45972  dvnprodlem3  45977