Theorem recnprss 24105

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 4420	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 10329	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 3845	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 250	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 3876	. . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
6	4, 5	jaoi 846	. 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
7	1, 6	syl 17	1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Syntax hints:   → wi 4   ∨ wo 836   = wceq 1601   ∈ wcel 2107   ⊆ wss 3792  {cpr 4400  ℂcc 10270  ℝcr 10271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754  ax-resscn 10329

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-un 3797  df-in 3799  df-ss 3806  df-sn 4399  df-pr 4401

This theorem is referenced by:  dvres3  24114  dvres3a  24115  dvcnp  24119  dvnff  24123  dvnadd  24129  dvnres  24131  cpnord  24135  cpncn  24136  cpnres  24137  dvadd  24140  dvmul  24141  dvaddf  24142  dvmulf  24143  dvcmul  24144  dvcmulf  24145  dvco  24147  dvcof  24148  dvmptid  24157  dvmptc  24158  dvmptres2  24162  dvmptcmul  24164  dvmptfsum  24175  dvcnvlem  24176  dvcnv  24177  dvlip2  24195  taylfvallem1  24548  tayl0  24553  taylply2  24559  taylply  24560  dvtaylp  24561  dvntaylp  24562  taylthlem1  24564  ulmdvlem1  24591  ulmdvlem3  24593  ulmdv  24594  dvsconst  39485  dvsid  39486  dvsef  39487  dvconstbi  39489  expgrowth  39490  dvdmsscn  41079  dvnmptdivc  41081  dvnmptconst  41084  dvnxpaek  41085  dvnmul  41086  dvnprodlem3  41091