Theorem recnprss 25654

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 4650	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 11171	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 4007	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 258	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 4040	. . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
6	4, 5	jaoi 854	. 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
7	1, 6	syl 17	1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Syntax hints:   → wi 4   ∨ wo 844   = wceq 1540   ∈ wcel 2105   ⊆ wss 3948  {cpr 4630  ℂcc 11112  ℝcr 11113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-resscn 11171

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-un 3953  df-in 3955  df-ss 3965  df-sn 4629  df-pr 4631

This theorem is referenced by:  dvres3  25663  dvres3a  25664  dvcnp  25669  dvnff  25674  dvnadd  25680  dvnres  25682  cpnord  25686  cpncn  25687  cpnres  25688  dvadd  25692  dvmul  25693  dvaddf  25694  dvmulf  25695  dvcmul  25696  dvcmulf  25697  dvco  25700  dvcof  25701  dvmptid  25710  dvmptc  25711  dvmptres2  25715  dvmptcmul  25717  dvmptfsum  25728  dvcnvlem  25729  dvcnv  25730  dvlip2  25748  taylfvallem1  26106  tayl0  26111  taylply2  26117  taylply  26118  dvtaylp  26119  dvntaylp  26120  taylthlem1  26122  ulmdvlem1  26149  ulmdvlem3  26151  ulmdv  26152  dvsconst  43392  dvsid  43393  dvsef  43394  dvconstbi  43396  expgrowth  43397  dvdmsscn  44951  dvnmptdivc  44953  dvnmptconst  44956  dvnxpaek  44957  dvnmul  44958  dvnprodlem3  44963