Theorem reelprrecn 11292

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

This proof depends on syntax axioms:   ∈ wcel 2145  {cpr 4586  ℂcc 11198  ℝcr 11199

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-cnex 11256  ax-resscn 11257

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-un 3904  df-in 3906  df-ss 3916  df-sn 4585  df-pr 4587

This theorem is used by:  dvf  26227  dvmptresicc  26236  dvmptcj  26288  dvmptre  26289  dvmptim  26290  rolle  26310  cmvth  26311  mvth  26312  dvlip  26313  dvlipcn  26314  dvle  26327  dvivthlem1  26328  dvivth  26330  lhop2  26335  dvcnvre  26339  dvfsumle  26341  dvfsumge  26342  dvfsumabs  26343  dvfsumlem2  26347  dvfsum2  26354  ftc2  26364  itgparts  26367  itgsubstlem  26368  itgpowd  26370  aalioulem3  26661  taylthlem2  26701  taylth  26702  efcvx  26776  pige3ALT  26848  dvrelog  26965  advlog  26982  advlogexp  26983  logccv  26991  dvcxp1  27068  loglesqrt  27089  divsqrtsumlem  27307  lgamgulmlem2  27357  logexprlim  27552  logdivsum  27860  log2sumbnd  27871  fdvneggt  35229  fdvnegge  35231  itgexpif  35235  logdivsqrle  35279  ftc2nc  38620  dvreasin  38624  dvreacos  38625  areacirclem1  38626  dvrelog2  43114  dvrelog3  43115  dvrelog2b  43116  dvrelogpow2b  43118  aks4d1p1p6  43123  redvmptabs  43411  readvrec2  43412  readvrec  43413  readvcot  43415  lhe4.4ex1a  45312  dvcosre  46921  dvcnre  46925  itgsin0pilem1  46959  itgsinexplem1  46963  itgcoscmulx  46978  itgiccshift  46989  itgperiod  46990  itgsbtaddcnst  46991  dirkeritg  47111  dirkercncflem2  47113  fourierdlem28  47144  fourierdlem39  47155  fourierdlem56  47171  fourierdlem57  47172  fourierdlem58  47173  fourierdlem59  47174  fourierdlem60  47175  fourierdlem61  47176  fourierdlem62  47177  fourierdlem68  47183  fourierdlem72  47187  fouriersw  47240  etransclem2  47245  etransclem23  47266  etransclem35  47278  etransclem38  47281  etransclem39  47282  etransclem44  47287  etransclem45  47288  etransclem46  47289  etransclem47  47290