Theorem reelprrecn 11116

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

Syntax hints:   ∈ wcel 2113  {cpr 4580  ℂcc 11022  ℝcr 11023

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-cnex 11080  ax-resscn 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-un 3904  df-in 3906  df-ss 3916  df-sn 4579  df-pr 4581

This theorem is referenced by:  dvf  25862  dvmptresicc  25871  dvmptcj  25926  dvmptre  25927  dvmptim  25928  rolle  25948  cmvth  25949  cmvthOLD  25950  mvth  25951  dvlip  25952  dvlipcn  25953  dvle  25966  dvivthlem1  25967  dvivth  25969  lhop2  25974  dvcnvre  25978  dvfsumle  25980  dvfsumleOLD  25981  dvfsumge  25982  dvfsumabs  25983  dvfsumlem2  25987  dvfsumlem2OLD  25988  dvfsum2  25995  ftc2  26005  itgparts  26008  itgsubstlem  26009  itgpowd  26011  aalioulem3  26296  taylthlem2  26336  taylthlem2OLD  26337  taylth  26338  efcvx  26413  pige3ALT  26483  dvrelog  26600  advlog  26617  advlogexp  26618  logccv  26626  dvcxp1  26703  loglesqrt  26725  divsqrtsumlem  26944  lgamgulmlem2  26994  logexprlim  27190  logdivsum  27498  log2sumbnd  27509  fdvneggt  34706  fdvnegge  34708  itgexpif  34712  logdivsqrle  34756  ftc2nc  37842  dvreasin  37846  dvreacos  37847  areacirclem1  37848  dvrelog2  42257  dvrelog3  42258  dvrelog2b  42259  dvrelogpow2b  42261  aks4d1p1p6  42266  redvmptabs  42557  readvrec2  42558  readvrec  42559  readvcot  42561  lhe4.4ex1a  44512  dvcosre  46098  dvcnre  46102  itgsin0pilem1  46136  itgsinexplem1  46140  itgcoscmulx  46155  itgiccshift  46166  itgperiod  46167  itgsbtaddcnst  46168  dirkeritg  46288  dirkercncflem2  46290  fourierdlem28  46321  fourierdlem39  46332  fourierdlem56  46348  fourierdlem57  46349  fourierdlem58  46350  fourierdlem59  46351  fourierdlem60  46352  fourierdlem61  46353  fourierdlem62  46354  fourierdlem68  46360  fourierdlem72  46364  fouriersw  46417  etransclem2  46422  etransclem23  46443  etransclem35  46455  etransclem38  46458  etransclem39  46459  etransclem44  46464  etransclem45  46465  etransclem46  46466  etransclem47  46467