Theorem recnprss 23474

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 4145	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 9872	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 3589	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 247	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 3620	. . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
6	4, 5	jaoi 393	. 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
7	1, 6	syl 17	1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Syntax hints:   → wi 4   ∨ wo 382   = wceq 1475   ∈ wcel 1977   ⊆ wss 3540  {cpr 4127  ℂcc 9813  ℝcr 9814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-resscn 9872

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554  df-sn 4126  df-pr 4128

This theorem is referenced by:  dvres3  23483  dvres3a  23484  dvcnp  23488  dvnff  23492  dvnadd  23498  dvnres  23500  cpnord  23504  cpncn  23505  cpnres  23506  dvadd  23509  dvmul  23510  dvaddf  23511  dvmulf  23512  dvcmul  23513  dvcmulf  23514  dvco  23516  dvcof  23517  dvmptid  23526  dvmptc  23527  dvmptres2  23531  dvmptcmul  23533  dvmptfsum  23542  dvcnvlem  23543  dvcnv  23544  dvlip2  23562  taylfvallem1  23915  tayl0  23920  taylply2  23926  taylply  23927  dvtaylp  23928  dvntaylp  23929  taylthlem1  23931  ulmdvlem1  23958  ulmdvlem3  23960  ulmdv  23961  dvsconst  37551  dvsid  37552  dvsef  37553  dvconstbi  37555  expgrowth  37556  dvdmsscn  38826  dvnmptdivc  38828  dvnmptconst  38831  dvnxpaek  38832  dvnmul  38833  dvnprodlem3  38838