Theorem reelprrecn 11276

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

Syntax hints:   ∈ wcel 2108  {cpr 4650  ℂcc 11182  ℝcr 11183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-cnex 11240  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-un 3981  df-in 3983  df-ss 3993  df-sn 4649  df-pr 4651

This theorem is referenced by:  dvf  25962  dvmptresicc  25971  dvmptcj  26026  dvmptre  26027  dvmptim  26028  rolle  26048  cmvth  26049  cmvthOLD  26050  mvth  26051  dvlip  26052  dvlipcn  26053  dvle  26066  dvivthlem1  26067  dvivth  26069  lhop2  26074  dvcnvre  26078  dvfsumle  26080  dvfsumleOLD  26081  dvfsumge  26082  dvfsumabs  26083  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsum2  26095  ftc2  26105  itgparts  26108  itgsubstlem  26109  itgpowd  26111  aalioulem3  26394  taylthlem2  26434  taylthlem2OLD  26435  taylth  26436  efcvx  26511  pige3ALT  26580  dvrelog  26697  advlog  26714  advlogexp  26715  logccv  26723  dvcxp1  26800  loglesqrt  26822  divsqrtsumlem  27041  lgamgulmlem2  27091  logexprlim  27287  logdivsum  27595  log2sumbnd  27606  fdvneggt  34577  fdvnegge  34579  itgexpif  34583  logdivsqrle  34627  ftc2nc  37662  dvreasin  37666  dvreacos  37667  areacirclem1  37668  dvrelog2  42021  dvrelog3  42022  dvrelog2b  42023  dvrelogpow2b  42025  aks4d1p1p6  42030  lhe4.4ex1a  44298  dvcosre  45833  dvcnre  45837  itgsin0pilem1  45871  itgsinexplem1  45875  itgcoscmulx  45890  itgiccshift  45901  itgperiod  45902  itgsbtaddcnst  45903  dirkeritg  46023  dirkercncflem2  46025  fourierdlem28  46056  fourierdlem39  46067  fourierdlem56  46083  fourierdlem57  46084  fourierdlem58  46085  fourierdlem59  46086  fourierdlem60  46087  fourierdlem61  46088  fourierdlem62  46089  fourierdlem68  46095  fourierdlem72  46099  fouriersw  46152  etransclem2  46157  etransclem23  46178  etransclem35  46190  etransclem38  46193  etransclem39  46194  etransclem44  46199  etransclem45  46200  etransclem46  46201  etransclem47  46202