Theorem reelprrecn 11136

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

Syntax hints:   ∈ wcel 2109  {cpr 4587  ℂcc 11042  ℝcr 11043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-cnex 11100  ax-resscn 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-un 3916  df-in 3918  df-ss 3928  df-sn 4586  df-pr 4588

This theorem is referenced by:  dvf  25841  dvmptresicc  25850  dvmptcj  25905  dvmptre  25906  dvmptim  25907  rolle  25927  cmvth  25928  cmvthOLD  25929  mvth  25930  dvlip  25931  dvlipcn  25932  dvle  25945  dvivthlem1  25946  dvivth  25948  lhop2  25953  dvcnvre  25957  dvfsumle  25959  dvfsumleOLD  25960  dvfsumge  25961  dvfsumabs  25962  dvfsumlem2  25966  dvfsumlem2OLD  25967  dvfsum2  25974  ftc2  25984  itgparts  25987  itgsubstlem  25988  itgpowd  25990  aalioulem3  26275  taylthlem2  26315  taylthlem2OLD  26316  taylth  26317  efcvx  26392  pige3ALT  26462  dvrelog  26579  advlog  26596  advlogexp  26597  logccv  26605  dvcxp1  26682  loglesqrt  26704  divsqrtsumlem  26923  lgamgulmlem2  26973  logexprlim  27169  logdivsum  27477  log2sumbnd  27488  fdvneggt  34584  fdvnegge  34586  itgexpif  34590  logdivsqrle  34634  ftc2nc  37689  dvreasin  37693  dvreacos  37694  areacirclem1  37695  dvrelog2  42045  dvrelog3  42046  dvrelog2b  42047  dvrelogpow2b  42049  aks4d1p1p6  42054  redvmptabs  42341  readvrec2  42342  readvrec  42343  readvcot  42345  lhe4.4ex1a  44311  dvcosre  45903  dvcnre  45907  itgsin0pilem1  45941  itgsinexplem1  45945  itgcoscmulx  45960  itgiccshift  45971  itgperiod  45972  itgsbtaddcnst  45973  dirkeritg  46093  dirkercncflem2  46095  fourierdlem28  46126  fourierdlem39  46137  fourierdlem56  46153  fourierdlem57  46154  fourierdlem58  46155  fourierdlem59  46156  fourierdlem60  46157  fourierdlem61  46158  fourierdlem62  46159  fourierdlem68  46165  fourierdlem72  46169  fouriersw  46222  etransclem2  46227  etransclem23  46248  etransclem35  46260  etransclem38  46263  etransclem39  46264  etransclem44  46269  etransclem45  46270  etransclem46  46271  etransclem47  46272