Theorem reelprrecn 11201

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

Syntax hints:   ∈ wcel 2106  {cpr 4630  ℂcc 11107  ℝcr 11108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-cnex 11165  ax-resscn 11166

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-un 3953  df-in 3955  df-ss 3965  df-sn 4629  df-pr 4631

This theorem is referenced by:  dvf  25423  dvmptresicc  25432  dvmptcj  25484  dvmptre  25485  dvmptim  25486  rolle  25506  cmvth  25507  mvth  25508  dvlip  25509  dvlipcn  25510  dvle  25523  dvivthlem1  25524  dvivth  25526  lhop2  25531  dvcnvre  25535  dvfsumle  25537  dvfsumge  25538  dvfsumabs  25539  dvfsumlem2  25543  dvfsum2  25550  ftc2  25560  itgparts  25563  itgsubstlem  25564  itgpowd  25566  aalioulem3  25846  taylthlem2  25885  taylth  25886  efcvx  25960  pige3ALT  26028  dvrelog  26144  advlog  26161  advlogexp  26162  logccv  26170  dvcxp1  26245  loglesqrt  26263  divsqrtsumlem  26481  lgamgulmlem2  26531  logexprlim  26725  logdivsum  27033  log2sumbnd  27044  fdvneggt  33607  fdvnegge  33609  itgexpif  33613  logdivsqrle  33657  gg-cmvth  35176  gg-dvfsumle  35177  gg-dvfsumlem2  35178  ftc2nc  36565  dvreasin  36569  dvreacos  36570  areacirclem1  36571  dvrelog2  40924  dvrelog3  40925  dvrelog2b  40926  dvrelogpow2b  40928  aks4d1p1p6  40933  lhe4.4ex1a  43078  dvcosre  44618  dvcnre  44622  itgsin0pilem1  44656  itgsinexplem1  44660  itgcoscmulx  44675  itgiccshift  44686  itgperiod  44687  itgsbtaddcnst  44688  dirkeritg  44808  dirkercncflem2  44810  fourierdlem28  44841  fourierdlem39  44852  fourierdlem56  44868  fourierdlem57  44869  fourierdlem58  44870  fourierdlem59  44871  fourierdlem60  44872  fourierdlem61  44873  fourierdlem62  44874  fourierdlem68  44880  fourierdlem72  44884  fouriersw  44937  etransclem2  44942  etransclem23  44963  etransclem35  44975  etransclem38  44978  etransclem39  44979  etransclem44  44984  etransclem45  44985  etransclem46  44986  etransclem47  44987