Theorem reelprrecn 10894

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

Syntax hints:   ∈ wcel 2108  {cpr 4560  ℂcc 10800  ℝcr 10801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-cnex 10858  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-sn 4559  df-pr 4561

This theorem is referenced by:  dvf  24976  dvmptresicc  24985  dvmptcj  25037  dvmptre  25038  dvmptim  25039  rolle  25059  cmvth  25060  mvth  25061  dvlip  25062  dvlipcn  25063  dvle  25076  dvivthlem1  25077  dvivth  25079  lhop2  25084  dvcnvre  25088  dvfsumle  25090  dvfsumge  25091  dvfsumabs  25092  dvfsumlem2  25096  dvfsum2  25103  ftc2  25113  itgparts  25116  itgsubstlem  25117  itgpowd  25119  aalioulem3  25399  taylthlem2  25438  taylth  25439  efcvx  25513  pige3ALT  25581  dvrelog  25697  advlog  25714  advlogexp  25715  logccv  25723  dvcxp1  25798  loglesqrt  25816  divsqrtsumlem  26034  lgamgulmlem2  26084  logexprlim  26278  logdivsum  26586  log2sumbnd  26597  fdvneggt  32480  fdvnegge  32482  itgexpif  32486  logdivsqrle  32530  ftc2nc  35786  dvreasin  35790  dvreacos  35791  areacirclem1  35792  dvrelog2  40000  dvrelog3  40001  dvrelog2b  40002  dvrelogpow2b  40004  aks4d1p1p6  40009  lhe4.4ex1a  41836  dvcosre  43343  dvcnre  43347  itgsin0pilem1  43381  itgsinexplem1  43385  itgcoscmulx  43400  itgiccshift  43411  itgperiod  43412  itgsbtaddcnst  43413  dirkeritg  43533  dirkercncflem2  43535  fourierdlem28  43566  fourierdlem39  43577  fourierdlem56  43593  fourierdlem57  43594  fourierdlem58  43595  fourierdlem59  43596  fourierdlem60  43597  fourierdlem61  43598  fourierdlem62  43599  fourierdlem68  43605  fourierdlem72  43609  fouriersw  43662  etransclem2  43667  etransclem23  43688  etransclem35  43700  etransclem38  43703  etransclem39  43704  etransclem44  43709  etransclem45  43710  etransclem46  43711  etransclem47  43712