Theorem reelprrecn 11191

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

Syntax hints:   ∈ wcel 2149  {cpr 4596  ℂcc 11097  ℝcr 11098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-cnex 11155  ax-resscn 11156

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-un 3918  df-in 3920  df-ss 3930  df-sn 4595  df-pr 4597

This theorem is referenced by:  dvf  26034  dvmptresicc  26043  dvmptcj  26095  dvmptre  26096  dvmptim  26097  rolle  26117  cmvth  26118  mvth  26119  dvlip  26120  dvlipcn  26121  dvle  26134  dvivthlem1  26135  dvivth  26137  lhop2  26142  dvcnvre  26146  dvfsumle  26148  dvfsumge  26149  dvfsumabs  26150  dvfsumlem2  26154  dvfsum2  26161  ftc2  26171  itgparts  26174  itgsubstlem  26175  itgpowd  26177  aalioulem3  26463  taylthlem2  26502  taylth  26503  efcvx  26577  pige3ALT  26650  dvrelog  26767  advlog  26784  advlogexp  26785  logccv  26793  dvcxp1  26870  loglesqrt  26891  divsqrtsumlem  27109  lgamgulmlem2  27159  logexprlim  27354  logdivsum  27662  log2sumbnd  27673  fdvneggt  34931  fdvnegge  34933  itgexpif  34937  logdivsqrle  34981  ftc2nc  38240  dvreasin  38244  dvreacos  38245  areacirclem1  38246  dvrelog2  42720  dvrelog3  42721  dvrelog2b  42722  dvrelogpow2b  42724  aks4d1p1p6  42729  redvmptabs  43010  readvrec2  43011  readvrec  43012  readvcot  43014  lhe4.4ex1a  44930  dvcosre  46517  dvcnre  46521  itgsin0pilem1  46555  itgsinexplem1  46559  itgcoscmulx  46574  itgiccshift  46585  itgperiod  46586  itgsbtaddcnst  46587  dirkeritg  46707  dirkercncflem2  46709  fourierdlem28  46740  fourierdlem39  46751  fourierdlem56  46767  fourierdlem57  46768  fourierdlem58  46769  fourierdlem59  46770  fourierdlem60  46771  fourierdlem61  46772  fourierdlem62  46773  fourierdlem68  46779  fourierdlem72  46783  fouriersw  46836  etransclem2  46841  etransclem23  46862  etransclem35  46874  etransclem38  46877  etransclem39  46878  etransclem44  46883  etransclem45  46884  etransclem46  46885  etransclem47  46886