Theorem reelprrecn 11098

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

Syntax hints:   ∈ wcel 2111  {cpr 4575  ℂcc 11004  ℝcr 11005

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-cnex 11062  ax-resscn 11063

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-un 3902  df-in 3904  df-ss 3914  df-sn 4574  df-pr 4576

This theorem is referenced by:  dvf  25835  dvmptresicc  25844  dvmptcj  25899  dvmptre  25900  dvmptim  25901  rolle  25921  cmvth  25922  cmvthOLD  25923  mvth  25924  dvlip  25925  dvlipcn  25926  dvle  25939  dvivthlem1  25940  dvivth  25942  lhop2  25947  dvcnvre  25951  dvfsumle  25953  dvfsumleOLD  25954  dvfsumge  25955  dvfsumabs  25956  dvfsumlem2  25960  dvfsumlem2OLD  25961  dvfsum2  25968  ftc2  25978  itgparts  25981  itgsubstlem  25982  itgpowd  25984  aalioulem3  26269  taylthlem2  26309  taylthlem2OLD  26310  taylth  26311  efcvx  26386  pige3ALT  26456  dvrelog  26573  advlog  26590  advlogexp  26591  logccv  26599  dvcxp1  26676  loglesqrt  26698  divsqrtsumlem  26917  lgamgulmlem2  26967  logexprlim  27163  logdivsum  27471  log2sumbnd  27482  fdvneggt  34613  fdvnegge  34615  itgexpif  34619  logdivsqrle  34663  ftc2nc  37752  dvreasin  37756  dvreacos  37757  areacirclem1  37758  dvrelog2  42167  dvrelog3  42168  dvrelog2b  42169  dvrelogpow2b  42171  aks4d1p1p6  42176  redvmptabs  42463  readvrec2  42464  readvrec  42465  readvcot  42467  lhe4.4ex1a  44432  dvcosre  46020  dvcnre  46024  itgsin0pilem1  46058  itgsinexplem1  46062  itgcoscmulx  46077  itgiccshift  46088  itgperiod  46089  itgsbtaddcnst  46090  dirkeritg  46210  dirkercncflem2  46212  fourierdlem28  46243  fourierdlem39  46254  fourierdlem56  46270  fourierdlem57  46271  fourierdlem58  46272  fourierdlem59  46273  fourierdlem60  46274  fourierdlem61  46275  fourierdlem62  46276  fourierdlem68  46282  fourierdlem72  46286  fouriersw  46339  etransclem2  46344  etransclem23  46365  etransclem35  46377  etransclem38  46380  etransclem39  46381  etransclem44  46386  etransclem45  46387  etransclem46  46388  etransclem47  46389