Theorem reelprrecn 11118

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

Syntax hints:   ∈ wcel 2113  {cpr 4582  ℂcc 11024  ℝcr 11025

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-cnex 11082  ax-resscn 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-un 3906  df-in 3908  df-ss 3918  df-sn 4581  df-pr 4583

This theorem is referenced by:  dvf  25864  dvmptresicc  25873  dvmptcj  25928  dvmptre  25929  dvmptim  25930  rolle  25950  cmvth  25951  cmvthOLD  25952  mvth  25953  dvlip  25954  dvlipcn  25955  dvle  25968  dvivthlem1  25969  dvivth  25971  lhop2  25976  dvcnvre  25980  dvfsumle  25982  dvfsumleOLD  25983  dvfsumge  25984  dvfsumabs  25985  dvfsumlem2  25989  dvfsumlem2OLD  25990  dvfsum2  25997  ftc2  26007  itgparts  26010  itgsubstlem  26011  itgpowd  26013  aalioulem3  26298  taylthlem2  26338  taylthlem2OLD  26339  taylth  26340  efcvx  26415  pige3ALT  26485  dvrelog  26602  advlog  26619  advlogexp  26620  logccv  26628  dvcxp1  26705  loglesqrt  26727  divsqrtsumlem  26946  lgamgulmlem2  26996  logexprlim  27192  logdivsum  27500  log2sumbnd  27511  fdvneggt  34757  fdvnegge  34759  itgexpif  34763  logdivsqrle  34807  ftc2nc  37903  dvreasin  37907  dvreacos  37908  areacirclem1  37909  dvrelog2  42318  dvrelog3  42319  dvrelog2b  42320  dvrelogpow2b  42322  aks4d1p1p6  42327  redvmptabs  42615  readvrec2  42616  readvrec  42617  readvcot  42619  lhe4.4ex1a  44570  dvcosre  46156  dvcnre  46160  itgsin0pilem1  46194  itgsinexplem1  46198  itgcoscmulx  46213  itgiccshift  46224  itgperiod  46225  itgsbtaddcnst  46226  dirkeritg  46346  dirkercncflem2  46348  fourierdlem28  46379  fourierdlem39  46390  fourierdlem56  46406  fourierdlem57  46407  fourierdlem58  46408  fourierdlem59  46409  fourierdlem60  46410  fourierdlem61  46411  fourierdlem62  46412  fourierdlem68  46418  fourierdlem72  46422  fouriersw  46475  etransclem2  46480  etransclem23  46501  etransclem35  46513  etransclem38  46516  etransclem39  46517  etransclem44  46522  etransclem45  46523  etransclem46  46524  etransclem47  46525