Theorem recnprss 25881

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 4592	. 2 ⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 = ℝ ∨ 𝑆 = ℂ))
2		ax-resscn 11086	. . . 4 ⊢ ℝ ⊆ ℂ
3		sseq1 3948	. . . 4 ⊢ (𝑆 = ℝ → (𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ))
4	2, 3	mpbiri 258	. . 3 ⊢ (𝑆 = ℝ → 𝑆 ⊆ ℂ)
5		eqimss 3981	. . 3 ⊢ (𝑆 = ℂ → 𝑆 ⊆ ℂ)
6	4, 5	jaoi 858	. 2 ⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → 𝑆 ⊆ ℂ)
7	1, 6	syl 17	1 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)

Syntax hints:   → wi 4   ∨ wo 848   = wceq 1542   ∈ wcel 2114   ⊆ wss 3890  {cpr 4570  ℂcc 11027  ℝcr 11028

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907  df-sn 4569  df-pr 4571

This theorem is referenced by:  dvres3  25890  dvres3a  25891  dvcnp  25896  dvnff  25900  dvnadd  25906  dvnres  25908  cpnord  25912  cpncn  25913  cpnres  25914  dvadd  25917  dvmul  25918  dvaddf  25919  dvmulf  25920  dvcmul  25921  dvcmulf  25922  dvco  25924  dvcof  25925  dvmptid  25934  dvmptc  25935  dvmptres2  25939  dvmptcmul  25941  dvmptfsum  25952  dvcnvlem  25953  dvcnv  25954  dvlip2  25972  taylfvallem1  26333  tayl0  26338  taylply2  26344  taylply2OLD  26345  taylply  26346  dvtaylp  26347  dvntaylp  26348  taylthlem1  26350  ulmdvlem1  26378  ulmdvlem3  26380  ulmdv  26381  dvsconst  44775  dvsid  44776  dvsef  44777  dvconstbi  44779  expgrowth  44780  dvdmsscn  46382  dvnmptdivc  46384  dvnmptconst  46387  dvnxpaek  46388  dvnmul  46389  dvnprodlem3  46394