Theorem reelprrecn 11184

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

Syntax hints:   ∈ wcel 2106  {cpr 4624  ℂcc 11090  ℝcr 11091

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 2702  ax-sep 5292  ax-cnex 11148  ax-resscn 11149

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 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-un 3949  df-in 3951  df-ss 3961  df-sn 4623  df-pr 4625

This theorem is referenced by:  dvf  25353  dvmptresicc  25362  dvmptcj  25414  dvmptre  25415  dvmptim  25416  rolle  25436  cmvth  25437  mvth  25438  dvlip  25439  dvlipcn  25440  dvle  25453  dvivthlem1  25454  dvivth  25456  lhop2  25461  dvcnvre  25465  dvfsumle  25467  dvfsumge  25468  dvfsumabs  25469  dvfsumlem2  25473  dvfsum2  25480  ftc2  25490  itgparts  25493  itgsubstlem  25494  itgpowd  25496  aalioulem3  25776  taylthlem2  25815  taylth  25816  efcvx  25890  pige3ALT  25958  dvrelog  26074  advlog  26091  advlogexp  26092  logccv  26100  dvcxp1  26175  loglesqrt  26193  divsqrtsumlem  26411  lgamgulmlem2  26461  logexprlim  26655  logdivsum  26963  log2sumbnd  26974  fdvneggt  33443  fdvnegge  33445  itgexpif  33449  logdivsqrle  33493  ftc2nc  36374  dvreasin  36378  dvreacos  36379  areacirclem1  36380  dvrelog2  40734  dvrelog3  40735  dvrelog2b  40736  dvrelogpow2b  40738  aks4d1p1p6  40743  lhe4.4ex1a  42859  dvcosre  44401  dvcnre  44405  itgsin0pilem1  44439  itgsinexplem1  44443  itgcoscmulx  44458  itgiccshift  44469  itgperiod  44470  itgsbtaddcnst  44471  dirkeritg  44591  dirkercncflem2  44593  fourierdlem28  44624  fourierdlem39  44635  fourierdlem56  44651  fourierdlem57  44652  fourierdlem58  44653  fourierdlem59  44654  fourierdlem60  44655  fourierdlem61  44656  fourierdlem62  44657  fourierdlem68  44663  fourierdlem72  44667  fouriersw  44720  etransclem2  44725  etransclem23  44746  etransclem35  44758  etransclem38  44761  etransclem39  44762  etransclem44  44767  etransclem45  44768  etransclem46  44769  etransclem47  44770