Theorem recnprss 25873

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

Syntax hints:   → wi 4   ∨ wo 848   = wceq 1542   ∈ wcel 2114   ⊆ wss 3903  {cpr 4584  ℂcc 11036  ℝcr 11037

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 11095

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 3444  df-un 3908  df-ss 3920  df-sn 4583  df-pr 4585

This theorem is referenced by:  dvres3  25882  dvres3a  25883  dvcnp  25888  dvnff  25893  dvnadd  25899  dvnres  25901  cpnord  25905  cpncn  25906  cpnres  25907  dvadd  25911  dvmul  25912  dvaddf  25913  dvmulf  25914  dvcmul  25915  dvcmulf  25916  dvco  25919  dvcof  25920  dvmptid  25929  dvmptc  25930  dvmptres2  25934  dvmptcmul  25936  dvmptfsum  25947  dvcnvlem  25948  dvcnv  25949  dvlip2  25968  taylfvallem1  26332  tayl0  26337  taylply2  26343  taylply2OLD  26344  taylply  26345  dvtaylp  26346  dvntaylp  26347  taylthlem1  26349  ulmdvlem1  26377  ulmdvlem3  26379  ulmdv  26380  dvsconst  44680  dvsid  44681  dvsef  44682  dvconstbi  44684  expgrowth  44685  dvdmsscn  46288  dvnmptdivc  46290  dvnmptconst  46293  dvnxpaek  46294  dvnmul  46295  dvnprodlem3  46300