Theorem recnprss 25068

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 4583	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 10928	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 3946	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 257	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 3977	. . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
6	4, 5	jaoi 854	. 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
7	1, 6	syl 17	1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Syntax hints:   → wi 4   ∨ wo 844   = wceq 1539   ∈ wcel 2106   ⊆ wss 3887  {cpr 4563  ℂcc 10869  ℝcr 10870

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-resscn 10928

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-in 3894  df-ss 3904  df-sn 4562  df-pr 4564

This theorem is referenced by:  dvres3  25077  dvres3a  25078  dvcnp  25083  dvnff  25087  dvnadd  25093  dvnres  25095  cpnord  25099  cpncn  25100  cpnres  25101  dvadd  25104  dvmul  25105  dvaddf  25106  dvmulf  25107  dvcmul  25108  dvcmulf  25109  dvco  25111  dvcof  25112  dvmptid  25121  dvmptc  25122  dvmptres2  25126  dvmptcmul  25128  dvmptfsum  25139  dvcnvlem  25140  dvcnv  25141  dvlip2  25159  taylfvallem1  25516  tayl0  25521  taylply2  25527  taylply  25528  dvtaylp  25529  dvntaylp  25530  taylthlem1  25532  ulmdvlem1  25559  ulmdvlem3  25561  ulmdv  25562  dvsconst  41948  dvsid  41949  dvsef  41950  dvconstbi  41952  expgrowth  41953  dvdmsscn  43477  dvnmptdivc  43479  dvnmptconst  43482  dvnxpaek  43483  dvnmul  43484  dvnprodlem3  43489