Theorem reelprrecn 11221

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

Syntax hints:   ∈ wcel 2108  {cpr 4603  ℂcc 11127  ℝcr 11128

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-cnex 11185  ax-resscn 11186

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-un 3931  df-in 3933  df-ss 3943  df-sn 4602  df-pr 4604

This theorem is referenced by:  dvf  25860  dvmptresicc  25869  dvmptcj  25924  dvmptre  25925  dvmptim  25926  rolle  25946  cmvth  25947  cmvthOLD  25948  mvth  25949  dvlip  25950  dvlipcn  25951  dvle  25964  dvivthlem1  25965  dvivth  25967  lhop2  25972  dvcnvre  25976  dvfsumle  25978  dvfsumleOLD  25979  dvfsumge  25980  dvfsumabs  25981  dvfsumlem2  25985  dvfsumlem2OLD  25986  dvfsum2  25993  ftc2  26003  itgparts  26006  itgsubstlem  26007  itgpowd  26009  aalioulem3  26294  taylthlem2  26334  taylthlem2OLD  26335  taylth  26336  efcvx  26411  pige3ALT  26481  dvrelog  26598  advlog  26615  advlogexp  26616  logccv  26624  dvcxp1  26701  loglesqrt  26723  divsqrtsumlem  26942  lgamgulmlem2  26992  logexprlim  27188  logdivsum  27496  log2sumbnd  27507  fdvneggt  34632  fdvnegge  34634  itgexpif  34638  logdivsqrle  34682  ftc2nc  37726  dvreasin  37730  dvreacos  37731  areacirclem1  37732  dvrelog2  42077  dvrelog3  42078  dvrelog2b  42079  dvrelogpow2b  42081  aks4d1p1p6  42086  redvmptabs  42403  readvrec2  42404  readvrec  42405  readvcot  42407  lhe4.4ex1a  44353  dvcosre  45941  dvcnre  45945  itgsin0pilem1  45979  itgsinexplem1  45983  itgcoscmulx  45998  itgiccshift  46009  itgperiod  46010  itgsbtaddcnst  46011  dirkeritg  46131  dirkercncflem2  46133  fourierdlem28  46164  fourierdlem39  46175  fourierdlem56  46191  fourierdlem57  46192  fourierdlem58  46193  fourierdlem59  46194  fourierdlem60  46195  fourierdlem61  46196  fourierdlem62  46197  fourierdlem68  46203  fourierdlem72  46207  fouriersw  46260  etransclem2  46265  etransclem23  46286  etransclem35  46298  etransclem38  46301  etransclem39  46302  etransclem44  46307  etransclem45  46308  etransclem46  46309  etransclem47  46310