Theorem reelprrecn 11165

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

Syntax hints:   ∈ wcel 2142  {cpr 4584  ℂcc 11071  ℝcr 11072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-cnex 11129  ax-resscn 11130

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-un 3909  df-in 3911  df-ss 3921  df-sn 4583  df-pr 4585

This theorem is referenced by:  dvf  25969  dvmptresicc  25978  dvmptcj  26030  dvmptre  26031  dvmptim  26032  rolle  26052  cmvth  26053  mvth  26054  dvlip  26055  dvlipcn  26056  dvle  26069  dvivthlem1  26070  dvivth  26072  lhop2  26077  dvcnvre  26081  dvfsumle  26083  dvfsumge  26084  dvfsumabs  26085  dvfsumlem2  26089  dvfsum2  26096  ftc2  26106  itgparts  26109  itgsubstlem  26110  itgpowd  26112  aalioulem3  26398  taylthlem2  26437  taylth  26438  efcvx  26512  pige3ALT  26585  dvrelog  26702  advlog  26719  advlogexp  26720  logccv  26728  dvcxp1  26805  loglesqrt  26826  divsqrtsumlem  27044  lgamgulmlem2  27094  logexprlim  27289  logdivsum  27597  log2sumbnd  27608  fdvneggt  34894  fdvnegge  34896  itgexpif  34900  logdivsqrle  34944  ftc2nc  38201  dvreasin  38205  dvreacos  38206  areacirclem1  38207  dvrelog2  42681  dvrelog3  42682  dvrelog2b  42683  dvrelogpow2b  42685  aks4d1p1p6  42690  redvmptabs  42969  readvrec2  42970  readvrec  42971  readvcot  42973  lhe4.4ex1a  44905  dvcosre  46486  dvcnre  46490  itgsin0pilem1  46524  itgsinexplem1  46528  itgcoscmulx  46543  itgiccshift  46554  itgperiod  46555  itgsbtaddcnst  46556  dirkeritg  46676  dirkercncflem2  46678  fourierdlem28  46709  fourierdlem39  46720  fourierdlem56  46736  fourierdlem57  46737  fourierdlem58  46738  fourierdlem59  46739  fourierdlem60  46740  fourierdlem61  46741  fourierdlem62  46742  fourierdlem68  46748  fourierdlem72  46752  fouriersw  46805  etransclem2  46810  etransclem23  46831  etransclem35  46843  etransclem38  46846  etransclem39  46847  etransclem44  46852  etransclem45  46853  etransclem46  46854  etransclem47  46855