Theorem recnprss 24504

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

Syntax hints:   → wi 4   ∨ wo 843   = wceq 1537   ∈ wcel 2114   ⊆ wss 3938  {cpr 4571  ℂcc 10537  ℝcr 10538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-resscn 10596

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-un 3943  df-in 3945  df-ss 3954  df-sn 4570  df-pr 4572

This theorem is referenced by:  dvres3  24513  dvres3a  24514  dvcnp  24518  dvnff  24522  dvnadd  24528  dvnres  24530  cpnord  24534  cpncn  24535  cpnres  24536  dvadd  24539  dvmul  24540  dvaddf  24541  dvmulf  24542  dvcmul  24543  dvcmulf  24544  dvco  24546  dvcof  24547  dvmptid  24556  dvmptc  24557  dvmptres2  24561  dvmptcmul  24563  dvmptfsum  24574  dvcnvlem  24575  dvcnv  24576  dvlip2  24594  taylfvallem1  24947  tayl0  24952  taylply2  24958  taylply  24959  dvtaylp  24960  dvntaylp  24961  taylthlem1  24963  ulmdvlem1  24990  ulmdvlem3  24992  ulmdv  24993  dvsconst  40669  dvsid  40670  dvsef  40671  dvconstbi  40673  expgrowth  40674  dvdmsscn  42228  dvnmptdivc  42230  dvnmptconst  42233  dvnxpaek  42234  dvnmul  42235  dvnprodlem3  42240