Theorem reelprrecn 11299

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

This proof depends on syntax axioms:   ∈ wcel 2144  {cpr 4586  ℂcc 11205  ℝcr 11206

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-cnex 11263  ax-resscn 11264

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-in 4090  df-un 4150  df-sn 4585  df-pr 4587

This theorem is used by:  dvf  26236  dvmptresicc  26245  dvmptcj  26297  dvmptre  26298  dvmptim  26299  rolle  26319  cmvth  26320  mvth  26321  dvlip  26322  dvlipcn  26323  dvle  26336  dvivthlem1  26337  dvivth  26339  lhop2  26344  dvcnvre  26348  dvfsumle  26350  dvfsumge  26351  dvfsumabs  26352  dvfsumlem2  26356  dvfsum2  26363  ftc2  26373  itgparts  26376  itgsubstlem  26377  itgpowd  26379  aalioulem3  26670  taylthlem2  26710  taylth  26711  efcvx  26785  pige3ALT  26857  dvrelog  26974  advlog  26991  advlogexp  26992  logccv  27000  dvcxp1  27077  loglesqrt  27098  divsqrtsumlem  27316  lgamgulmlem2  27366  logexprlim  27561  logdivsum  27869  log2sumbnd  27880  fdvneggt  35279  fdvnegge  35281  itgexpif  35285  logdivsqrle  35329  ftc2nc  38757  dvreasin  38761  dvreacos  38762  areacirclem1  38763  dvrelog2  43251  dvrelog3  43252  dvrelog2b  43253  dvrelogpow2b  43255  aks4d1p1p6  43260  redvmptabs  43548  readvrec2  43549  readvrec  43550  readvcot  43552  lhe4.4ex1a  45450  dvcosre  47058  dvcnre  47062  itgsin0pilem1  47096  itgsinexplem1  47100  itgcoscmulx  47115  itgiccshift  47126  itgperiod  47127  itgsbtaddcnst  47128  dirkeritg  47248  dirkercncflem2  47250  fourierdlem28  47281  fourierdlem39  47292  fourierdlem56  47308  fourierdlem57  47309  fourierdlem58  47310  fourierdlem59  47311  fourierdlem60  47312  fourierdlem61  47313  fourierdlem62  47314  fourierdlem68  47320  fourierdlem72  47324  fouriersw  47377  etransclem2  47382  etransclem23  47403  etransclem35  47415  etransclem38  47418  etransclem39  47419  etransclem44  47424  etransclem45  47425  etransclem46  47426  etransclem47  47427