Theorem reelprrecn 11331

Description: Reals are a subset of the pair of real and complex numbers. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
reelprrecn	⊢ ℝ ∈ {ℝ, ℂ}

Proof of Theorem reelprrecn

Step	Hyp	Ref	Expression
1		reex 11330	. 2 ⊢ ℝ ∈ V
2	1	prid1 4725	1 ⊢ ℝ ∈ {ℝ, ℂ}

This proof depends on syntax axioms:   ∈ wcel 2147  {cpr 4590  ℂcc 11237  ℝcr 11238

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-cnex 11295  ax-resscn 11296

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  dvf  26282  dvmptresicc  26291  dvmptcj  26343  dvmptre  26344  dvmptim  26345  rolle  26365  cmvth  26366  mvth  26367  dvlip  26368  dvlipcn  26369  dvle  26382  dvivthlem1  26383  dvivth  26385  lhop2  26390  dvcnvre  26394  dvfsumle  26396  dvfsumge  26397  dvfsumabs  26398  dvfsumlem2  26402  dvfsum2  26409  ftc2  26419  itgparts  26422  itgsubstlem  26423  itgpowd  26425  aalioulem3  26718  taylthlem2  26758  taylth  26759  efcvx  26833  pige3ALT  26905  dvrelog  27022  advlog  27039  advlogexp  27040  logccv  27048  dvcxp1  27125  loglesqrt  27146  divsqrtsumlem  27364  lgamgulmlem2  27414  logexprlim  27609  logdivsum  27917  log2sumbnd  27928  fdvneggt  35340  fdvnegge  35342  itgexpif  35346  logdivsqrle  35390  ftc2nc  38888  dvreasin  38892  dvreacos  38893  areacirclem1  38894  dvrelog2  43380  dvrelog3  43381  dvrelog2b  43382  dvrelogpow2b  43384  aks4d1p1p6  43389  redvmptabs  43677  readvrec2  43678  readvrec  43679  readvcot  43681  lhe4.4ex1a  45574  dvcosre  47195  dvcnre  47199  itgsin0pilem1  47233  itgsinexplem1  47237  itgcoscmulx  47252  itgiccshift  47263  itgperiod  47264  itgsbtaddcnst  47265  dirkeritg  47385  dirkercncflem2  47387  fourierdlem28  47418  fourierdlem39  47429  fourierdlem56  47445  fourierdlem57  47446  fourierdlem58  47447  fourierdlem59  47448  fourierdlem60  47449  fourierdlem61  47450  fourierdlem62  47451  fourierdlem68  47457  fourierdlem72  47461  fouriersw  47514  etransclem2  47519  etransclem23  47540  etransclem35  47552  etransclem38  47555  etransclem39  47556  etransclem44  47561  etransclem45  47562  etransclem46  47563  etransclem47  47564