Theorem recnprss 26138

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 4611	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 11185	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 3959	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 261	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 3992	. . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
6	4, 5	jaoi 871	. 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
7	1, 6	syl 18	1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1570   ∈ wcel 2145   ⊆ wss 3902  {cpr 4589  ℂcc 11126  ℝcr 11127

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-resscn 11185

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919  df-sn 4588  df-pr 4590

This theorem is used by:  dvres3  26147  dvres3a  26148  dvcnp  26153  dvnff  26157  dvnadd  26163  dvnres  26165  cpnord  26169  cpncn  26170  cpnres  26171  dvadd  26174  dvmul  26175  dvaddf  26176  dvmulf  26177  dvcmul  26178  dvcmulf  26179  dvco  26181  dvcof  26182  dvmptid  26191  dvmptc  26192  dvmptres2  26196  dvmptcmul  26198  dvmptfsum  26209  dvcnvlem  26210  dvcnv  26211  dvlip2  26229  taylfvallem1  26600  tayl0  26605  taylply2  26611  taylply  26612  dvtaylp  26613  dvntaylp  26614  taylthlem1  26616  ulmdvlem1  26643  ulmdvlem3  26645  ulmdv  26646  dvsconst  45162  dvsid  45163  dvsef  45164  dvconstbi  45166  expgrowth  45167  dvdmsscn  46772  dvnmptdivc  46774  dvnmptconst  46777  dvnxpaek  46778  dvnmul  46779  dvnprodlem3  46784