Theorem reelprrecn 11101

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

Syntax hints:   ∈ wcel 2109  {cpr 4579  ℂcc 11007  ℝcr 11008

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 5235  ax-cnex 11065  ax-resscn 11066

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 3395  df-v 3438  df-un 3908  df-in 3910  df-ss 3920  df-sn 4578  df-pr 4580

This theorem is referenced by:  dvf  25806  dvmptresicc  25815  dvmptcj  25870  dvmptre  25871  dvmptim  25872  rolle  25892  cmvth  25893  cmvthOLD  25894  mvth  25895  dvlip  25896  dvlipcn  25897  dvle  25910  dvivthlem1  25911  dvivth  25913  lhop2  25918  dvcnvre  25922  dvfsumle  25924  dvfsumleOLD  25925  dvfsumge  25926  dvfsumabs  25927  dvfsumlem2  25931  dvfsumlem2OLD  25932  dvfsum2  25939  ftc2  25949  itgparts  25952  itgsubstlem  25953  itgpowd  25955  aalioulem3  26240  taylthlem2  26280  taylthlem2OLD  26281  taylth  26282  efcvx  26357  pige3ALT  26427  dvrelog  26544  advlog  26561  advlogexp  26562  logccv  26570  dvcxp1  26647  loglesqrt  26669  divsqrtsumlem  26888  lgamgulmlem2  26938  logexprlim  27134  logdivsum  27442  log2sumbnd  27453  fdvneggt  34568  fdvnegge  34570  itgexpif  34574  logdivsqrle  34618  ftc2nc  37682  dvreasin  37686  dvreacos  37687  areacirclem1  37688  dvrelog2  42037  dvrelog3  42038  dvrelog2b  42039  dvrelogpow2b  42041  aks4d1p1p6  42046  redvmptabs  42333  readvrec2  42334  readvrec  42335  readvcot  42337  lhe4.4ex1a  44302  dvcosre  45893  dvcnre  45897  itgsin0pilem1  45931  itgsinexplem1  45935  itgcoscmulx  45950  itgiccshift  45961  itgperiod  45962  itgsbtaddcnst  45963  dirkeritg  46083  dirkercncflem2  46085  fourierdlem28  46116  fourierdlem39  46127  fourierdlem56  46143  fourierdlem57  46144  fourierdlem58  46145  fourierdlem59  46146  fourierdlem60  46147  fourierdlem61  46148  fourierdlem62  46149  fourierdlem68  46155  fourierdlem72  46159  fouriersw  46212  etransclem2  46217  etransclem23  46238  etransclem35  46250  etransclem38  46253  etransclem39  46254  etransclem44  46259  etransclem45  46260  etransclem46  46261  etransclem47  46262