Theorem reelprrecn 11207

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

This proof depends on syntax axioms:   ∈ wcel 2146  {cpr 4593  ℂcc 11113  ℝcr 11114

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-cnex 11171  ax-resscn 11172

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-un 3911  df-in 3913  df-ss 3923  df-sn 4592  df-pr 4594

This theorem is used by:  dvf  26117  dvmptresicc  26126  dvmptcj  26178  dvmptre  26179  dvmptim  26180  rolle  26200  cmvth  26201  mvth  26202  dvlip  26203  dvlipcn  26204  dvle  26217  dvivthlem1  26218  dvivth  26220  lhop2  26225  dvcnvre  26229  dvfsumle  26231  dvfsumge  26232  dvfsumabs  26233  dvfsumlem2  26237  dvfsum2  26244  ftc2  26254  itgparts  26257  itgsubstlem  26258  itgpowd  26260  aalioulem3  26548  taylthlem2  26588  taylth  26589  efcvx  26663  pige3ALT  26736  dvrelog  26853  advlog  26870  advlogexp  26871  logccv  26879  dvcxp1  26956  loglesqrt  26977  divsqrtsumlem  27195  lgamgulmlem2  27245  logexprlim  27440  logdivsum  27748  log2sumbnd  27759  fdvneggt  35052  fdvnegge  35054  itgexpif  35058  logdivsqrle  35102  ftc2nc  38410  dvreasin  38414  dvreacos  38415  areacirclem1  38416  dvrelog2  42889  dvrelog3  42890  dvrelog2b  42891  dvrelogpow2b  42893  aks4d1p1p6  42898  redvmptabs  43179  readvrec2  43180  readvrec  43181  readvcot  43183  lhe4.4ex1a  45097  dvcosre  46684  dvcnre  46688  itgsin0pilem1  46722  itgsinexplem1  46726  itgcoscmulx  46741  itgiccshift  46752  itgperiod  46753  itgsbtaddcnst  46754  dirkeritg  46874  dirkercncflem2  46876  fourierdlem28  46907  fourierdlem39  46918  fourierdlem56  46934  fourierdlem57  46935  fourierdlem58  46936  fourierdlem59  46937  fourierdlem60  46938  fourierdlem61  46939  fourierdlem62  46940  fourierdlem68  46946  fourierdlem72  46950  fouriersw  47003  etransclem2  47008  etransclem23  47029  etransclem35  47041  etransclem38  47044  etransclem39  47045  etransclem44  47050  etransclem45  47051  etransclem46  47052  etransclem47  47053