Theorem reelprrecn 11130

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 11129	. 2 ⊢ ℝ ∈ V
2	1	prid1 4721	1 ⊢ ℝ ∈ {ℝ, ℂ}

Syntax hints:   ∈ wcel 2114  {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-sep 5243  ax-cnex 11094  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-un 3908  df-in 3910  df-ss 3920  df-sn 4583  df-pr 4585

This theorem is referenced by:  dvf  25876  dvmptresicc  25885  dvmptcj  25940  dvmptre  25941  dvmptim  25942  rolle  25962  cmvth  25963  cmvthOLD  25964  mvth  25965  dvlip  25966  dvlipcn  25967  dvle  25980  dvivthlem1  25981  dvivth  25983  lhop2  25988  dvcnvre  25992  dvfsumle  25994  dvfsumleOLD  25995  dvfsumge  25996  dvfsumabs  25997  dvfsumlem2  26001  dvfsumlem2OLD  26002  dvfsum2  26009  ftc2  26019  itgparts  26022  itgsubstlem  26023  itgpowd  26025  aalioulem3  26310  taylthlem2  26350  taylthlem2OLD  26351  taylth  26352  efcvx  26427  pige3ALT  26497  dvrelog  26614  advlog  26631  advlogexp  26632  logccv  26640  dvcxp1  26717  loglesqrt  26739  divsqrtsumlem  26958  lgamgulmlem2  27008  logexprlim  27204  logdivsum  27512  log2sumbnd  27523  fdvneggt  34778  fdvnegge  34780  itgexpif  34784  logdivsqrle  34828  ftc2nc  37953  dvreasin  37957  dvreacos  37958  areacirclem1  37959  dvrelog2  42434  dvrelog3  42435  dvrelog2b  42436  dvrelogpow2b  42438  aks4d1p1p6  42443  redvmptabs  42730  readvrec2  42731  readvrec  42732  readvcot  42734  lhe4.4ex1a  44685  dvcosre  46270  dvcnre  46274  itgsin0pilem1  46308  itgsinexplem1  46312  itgcoscmulx  46327  itgiccshift  46338  itgperiod  46339  itgsbtaddcnst  46340  dirkeritg  46460  dirkercncflem2  46462  fourierdlem28  46493  fourierdlem39  46504  fourierdlem56  46520  fourierdlem57  46521  fourierdlem58  46522  fourierdlem59  46523  fourierdlem60  46524  fourierdlem61  46525  fourierdlem62  46526  fourierdlem68  46532  fourierdlem72  46536  fouriersw  46589  etransclem2  46594  etransclem23  46615  etransclem35  46627  etransclem38  46630  etransclem39  46631  etransclem44  46636  etransclem45  46637  etransclem46  46638  etransclem47  46639