Theorem reelprrecn 11167

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

Syntax hints:   ∈ wcel 2109  {cpr 4594  ℂcc 11073  ℝcr 11074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-cnex 11131  ax-resscn 11132

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-un 3922  df-in 3924  df-ss 3934  df-sn 4593  df-pr 4595

This theorem is referenced by:  dvf  25815  dvmptresicc  25824  dvmptcj  25879  dvmptre  25880  dvmptim  25881  rolle  25901  cmvth  25902  cmvthOLD  25903  mvth  25904  dvlip  25905  dvlipcn  25906  dvle  25919  dvivthlem1  25920  dvivth  25922  lhop2  25927  dvcnvre  25931  dvfsumle  25933  dvfsumleOLD  25934  dvfsumge  25935  dvfsumabs  25936  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsum2  25948  ftc2  25958  itgparts  25961  itgsubstlem  25962  itgpowd  25964  aalioulem3  26249  taylthlem2  26289  taylthlem2OLD  26290  taylth  26291  efcvx  26366  pige3ALT  26436  dvrelog  26553  advlog  26570  advlogexp  26571  logccv  26579  dvcxp1  26656  loglesqrt  26678  divsqrtsumlem  26897  lgamgulmlem2  26947  logexprlim  27143  logdivsum  27451  log2sumbnd  27462  fdvneggt  34598  fdvnegge  34600  itgexpif  34604  logdivsqrle  34648  ftc2nc  37703  dvreasin  37707  dvreacos  37708  areacirclem1  37709  dvrelog2  42059  dvrelog3  42060  dvrelog2b  42061  dvrelogpow2b  42063  aks4d1p1p6  42068  redvmptabs  42355  readvrec2  42356  readvrec  42357  readvcot  42359  lhe4.4ex1a  44325  dvcosre  45917  dvcnre  45921  itgsin0pilem1  45955  itgsinexplem1  45959  itgcoscmulx  45974  itgiccshift  45985  itgperiod  45986  itgsbtaddcnst  45987  dirkeritg  46107  dirkercncflem2  46109  fourierdlem28  46140  fourierdlem39  46151  fourierdlem56  46167  fourierdlem57  46168  fourierdlem58  46169  fourierdlem59  46170  fourierdlem60  46171  fourierdlem61  46172  fourierdlem62  46173  fourierdlem68  46179  fourierdlem72  46183  fouriersw  46236  etransclem2  46241  etransclem23  46262  etransclem35  46274  etransclem38  46277  etransclem39  46278  etransclem44  46283  etransclem45  46284  etransclem46  46285  etransclem47  46286