Theorem recnprss 24507

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 4547	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 10583	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 3940	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 261	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 3971	. . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
6	4, 5	jaoi 854	. 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
7	1, 6	syl 17	1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Syntax hints:   → wi 4   ∨ wo 844   = wceq 1538   ∈ wcel 2111   ⊆ wss 3881  {cpr 4527  ℂcc 10524  ℝcr 10525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-resscn 10583

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528

This theorem is referenced by:  dvres3  24516  dvres3a  24517  dvcnp  24522  dvnff  24526  dvnadd  24532  dvnres  24534  cpnord  24538  cpncn  24539  cpnres  24540  dvadd  24543  dvmul  24544  dvaddf  24545  dvmulf  24546  dvcmul  24547  dvcmulf  24548  dvco  24550  dvcof  24551  dvmptid  24560  dvmptc  24561  dvmptres2  24565  dvmptcmul  24567  dvmptfsum  24578  dvcnvlem  24579  dvcnv  24580  dvlip2  24598  taylfvallem1  24952  tayl0  24957  taylply2  24963  taylply  24964  dvtaylp  24965  dvntaylp  24966  taylthlem1  24968  ulmdvlem1  24995  ulmdvlem3  24997  ulmdv  24998  dvsconst  41034  dvsid  41035  dvsef  41036  dvconstbi  41038  expgrowth  41039  dvdmsscn  42578  dvnmptdivc  42580  dvnmptconst  42583  dvnxpaek  42584  dvnmul  42585  dvnprodlem3  42590