Theorem recnprss 24496

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 4582	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 10588	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 3991	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 260	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 4022	. . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
6	4, 5	jaoi 853	. 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
7	1, 6	syl 17	1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Syntax hints:   → wi 4   ∨ wo 843   = wceq 1533   ∈ wcel 2110   ⊆ wss 3935  {cpr 4562  ℂcc 10529  ℝcr 10530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-resscn 10588

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3940  df-in 3942  df-ss 3951  df-sn 4561  df-pr 4563

This theorem is referenced by:  dvres3  24505  dvres3a  24506  dvcnp  24510  dvnff  24514  dvnadd  24520  dvnres  24522  cpnord  24526  cpncn  24527  cpnres  24528  dvadd  24531  dvmul  24532  dvaddf  24533  dvmulf  24534  dvcmul  24535  dvcmulf  24536  dvco  24538  dvcof  24539  dvmptid  24548  dvmptc  24549  dvmptres2  24553  dvmptcmul  24555  dvmptfsum  24566  dvcnvlem  24567  dvcnv  24568  dvlip2  24586  taylfvallem1  24939  tayl0  24944  taylply2  24950  taylply  24951  dvtaylp  24952  dvntaylp  24953  taylthlem1  24955  ulmdvlem1  24982  ulmdvlem3  24984  ulmdv  24985  dvsconst  40655  dvsid  40656  dvsef  40657  dvconstbi  40659  expgrowth  40660  dvdmsscn  42214  dvnmptdivc  42216  dvnmptconst  42219  dvnxpaek  42220  dvnmul  42221  dvnprodlem3  42226