Theorem reelprrecn 11245

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

Syntax hints:   ∈ wcel 2106  {cpr 4633  ℂcc 11151  ℝcr 11152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-cnex 11209  ax-resscn 11210

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-un 3968  df-in 3970  df-ss 3980  df-sn 4632  df-pr 4634

This theorem is referenced by:  dvf  25957  dvmptresicc  25966  dvmptcj  26021  dvmptre  26022  dvmptim  26023  rolle  26043  cmvth  26044  cmvthOLD  26045  mvth  26046  dvlip  26047  dvlipcn  26048  dvle  26061  dvivthlem1  26062  dvivth  26064  lhop2  26069  dvcnvre  26073  dvfsumle  26075  dvfsumleOLD  26076  dvfsumge  26077  dvfsumabs  26078  dvfsumlem2  26082  dvfsumlem2OLD  26083  dvfsum2  26090  ftc2  26100  itgparts  26103  itgsubstlem  26104  itgpowd  26106  aalioulem3  26391  taylthlem2  26431  taylthlem2OLD  26432  taylth  26433  efcvx  26508  pige3ALT  26577  dvrelog  26694  advlog  26711  advlogexp  26712  logccv  26720  dvcxp1  26797  loglesqrt  26819  divsqrtsumlem  27038  lgamgulmlem2  27088  logexprlim  27284  logdivsum  27592  log2sumbnd  27603  fdvneggt  34594  fdvnegge  34596  itgexpif  34600  logdivsqrle  34644  ftc2nc  37689  dvreasin  37693  dvreacos  37694  areacirclem1  37695  dvrelog2  42046  dvrelog3  42047  dvrelog2b  42048  dvrelogpow2b  42050  aks4d1p1p6  42055  redvmptabs  42369  readvrec2  42370  readvrec  42371  lhe4.4ex1a  44325  dvcosre  45868  dvcnre  45872  itgsin0pilem1  45906  itgsinexplem1  45910  itgcoscmulx  45925  itgiccshift  45936  itgperiod  45937  itgsbtaddcnst  45938  dirkeritg  46058  dirkercncflem2  46060  fourierdlem28  46091  fourierdlem39  46102  fourierdlem56  46118  fourierdlem57  46119  fourierdlem58  46120  fourierdlem59  46121  fourierdlem60  46122  fourierdlem61  46123  fourierdlem62  46124  fourierdlem68  46130  fourierdlem72  46134  fouriersw  46187  etransclem2  46192  etransclem23  46213  etransclem35  46225  etransclem38  46228  etransclem39  46229  etransclem44  46234  etransclem45  46235  etransclem46  46236  etransclem47  46237