Theorem reelprrecn 11202

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

Syntax hints:   ∈ wcel 2107  {cpr 4631  ℂcc 11108  ℝcr 11109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-cnex 11166  ax-resscn 11167

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-sn 4630  df-pr 4632

This theorem is referenced by:  dvf  25424  dvmptresicc  25433  dvmptcj  25485  dvmptre  25486  dvmptim  25487  rolle  25507  cmvth  25508  mvth  25509  dvlip  25510  dvlipcn  25511  dvle  25524  dvivthlem1  25525  dvivth  25527  lhop2  25532  dvcnvre  25536  dvfsumle  25538  dvfsumge  25539  dvfsumabs  25540  dvfsumlem2  25544  dvfsum2  25551  ftc2  25561  itgparts  25564  itgsubstlem  25565  itgpowd  25567  aalioulem3  25847  taylthlem2  25886  taylth  25887  efcvx  25961  pige3ALT  26029  dvrelog  26145  advlog  26162  advlogexp  26163  logccv  26171  dvcxp1  26248  loglesqrt  26266  divsqrtsumlem  26484  lgamgulmlem2  26534  logexprlim  26728  logdivsum  27036  log2sumbnd  27047  fdvneggt  33612  fdvnegge  33614  itgexpif  33618  logdivsqrle  33662  gg-cmvth  35181  gg-dvfsumle  35182  gg-dvfsumlem2  35183  ftc2nc  36570  dvreasin  36574  dvreacos  36575  areacirclem1  36576  dvrelog2  40929  dvrelog3  40930  dvrelog2b  40931  dvrelogpow2b  40933  aks4d1p1p6  40938  lhe4.4ex1a  43088  dvcosre  44628  dvcnre  44632  itgsin0pilem1  44666  itgsinexplem1  44670  itgcoscmulx  44685  itgiccshift  44696  itgperiod  44697  itgsbtaddcnst  44698  dirkeritg  44818  dirkercncflem2  44820  fourierdlem28  44851  fourierdlem39  44862  fourierdlem56  44878  fourierdlem57  44879  fourierdlem58  44880  fourierdlem59  44881  fourierdlem60  44882  fourierdlem61  44883  fourierdlem62  44884  fourierdlem68  44890  fourierdlem72  44894  fouriersw  44947  etransclem2  44952  etransclem23  44973  etransclem35  44985  etransclem38  44988  etransclem39  44989  etransclem44  44994  etransclem45  44995  etransclem46  44996  etransclem47  44997