Theorem reelprrecn 11187

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

Syntax hints:   ∈ wcel 2143  {cpr 4591  ℂcc 11093  ℝcr 11094

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-cnex 11151  ax-resscn 11152

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-un 3910  df-in 3912  df-ss 3922  df-sn 4590  df-pr 4592

This theorem is referenced by:  dvf  26066  dvmptresicc  26075  dvmptcj  26127  dvmptre  26128  dvmptim  26129  rolle  26149  cmvth  26150  mvth  26151  dvlip  26152  dvlipcn  26153  dvle  26166  dvivthlem1  26167  dvivth  26169  lhop2  26174  dvcnvre  26178  dvfsumle  26180  dvfsumge  26181  dvfsumabs  26182  dvfsumlem2  26186  dvfsum2  26193  ftc2  26203  itgparts  26206  itgsubstlem  26207  itgpowd  26209  aalioulem3  26497  taylthlem2  26537  taylth  26538  efcvx  26612  pige3ALT  26685  dvrelog  26802  advlog  26819  advlogexp  26820  logccv  26828  dvcxp1  26905  loglesqrt  26926  divsqrtsumlem  27144  lgamgulmlem2  27194  logexprlim  27389  logdivsum  27697  log2sumbnd  27708  fdvneggt  34987  fdvnegge  34989  itgexpif  34993  logdivsqrle  35037  ftc2nc  38353  dvreasin  38357  dvreacos  38358  areacirclem1  38359  dvrelog2  42831  dvrelog3  42832  dvrelog2b  42833  dvrelogpow2b  42835  aks4d1p1p6  42840  redvmptabs  43121  readvrec2  43122  readvrec  43123  readvcot  43125  lhe4.4ex1a  45039  dvcosre  46626  dvcnre  46630  itgsin0pilem1  46664  itgsinexplem1  46668  itgcoscmulx  46683  itgiccshift  46694  itgperiod  46695  itgsbtaddcnst  46696  dirkeritg  46816  dirkercncflem2  46818  fourierdlem28  46849  fourierdlem39  46860  fourierdlem56  46876  fourierdlem57  46877  fourierdlem58  46878  fourierdlem59  46879  fourierdlem60  46880  fourierdlem61  46881  fourierdlem62  46882  fourierdlem68  46888  fourierdlem72  46892  fouriersw  46945  etransclem2  46950  etransclem23  46971  etransclem35  46983  etransclem38  46986  etransclem39  46987  etransclem44  46992  etransclem45  46993  etransclem46  46994  etransclem47  46995