Theorem recnprss 23668

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 4197	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 9993	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 3626	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 248	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 3657	. . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
6	4, 5	jaoi 394	. 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
7	1, 6	syl 17	1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Syntax hints:   → wi 4   ∨ wo 383   = wceq 1483   ∈ wcel 1990   ⊆ wss 3574  {cpr 4179  ℂcc 9934  ℝcr 9935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-resscn 9993

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-in 3581  df-ss 3588  df-sn 4178  df-pr 4180

This theorem is referenced by:  dvres3  23677  dvres3a  23678  dvcnp  23682  dvnff  23686  dvnadd  23692  dvnres  23694  cpnord  23698  cpncn  23699  cpnres  23700  dvadd  23703  dvmul  23704  dvaddf  23705  dvmulf  23706  dvcmul  23707  dvcmulf  23708  dvco  23710  dvcof  23711  dvmptid  23720  dvmptc  23721  dvmptres2  23725  dvmptcmul  23727  dvmptfsum  23738  dvcnvlem  23739  dvcnv  23740  dvlip2  23758  taylfvallem1  24111  tayl0  24116  taylply2  24122  taylply  24123  dvtaylp  24124  dvntaylp  24125  taylthlem1  24127  ulmdvlem1  24154  ulmdvlem3  24156  ulmdv  24157  dvsconst  38529  dvsid  38530  dvsef  38531  dvconstbi  38533  expgrowth  38534  dvdmsscn  40151  dvnmptdivc  40153  dvnmptconst  40156  dvnxpaek  40157  dvnmul  40158  dvnprodlem3  40163