Theorem reelprrecn 9907

Description: Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
reelprrecn	⊢ ℝ ∈ {ℝ, ℂ}

Proof of Theorem reelprrecn

Step	Hyp	Ref	Expression
1		reex 9906	. 2 ⊢ ℝ ∈ V
2	1	prid1 4241	1 ⊢ ℝ ∈ {ℝ, ℂ}

Syntax hints:   ∈ wcel 1977  {cpr 4127  ℂcc 9813  ℝcr 9814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-cnex 9871  ax-resscn 9872

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554  df-sn 4126  df-pr 4128

This theorem is referenced by:  dvf  23477  dvmptcj  23537  dvmptre  23538  dvmptim  23539  rolle  23557  cmvth  23558  mvth  23559  dvlip  23560  dvlipcn  23561  dvle  23574  dvivthlem1  23575  dvivth  23577  lhop2  23582  dvcnvre  23586  dvfsumle  23588  dvfsumge  23589  dvfsumabs  23590  dvfsumlem2  23594  dvfsum2  23601  ftc2  23611  itgparts  23614  itgsubstlem  23615  aalioulem3  23893  taylthlem2  23932  taylth  23933  efcvx  24007  pige3  24073  dvrelog  24183  advlog  24200  advlogexp  24201  logccv  24209  dvcxp1  24281  loglesqrt  24299  divsqrtsumlem  24506  lgamgulmlem2  24556  logexprlim  24750  logdivsum  25022  log2sumbnd  25033  ftc2nc  32664  dvreasin  32668  dvreacos  32669  areacirclem1  32670  itgpowd  36819  lhe4.4ex1a  37550  dvcosre  38799  dvcnre  38804  dvmptresicc  38809  itgsin0pilem1  38841  itgsinexplem1  38845  itgcoscmulx  38861  itgiccshift  38872  itgperiod  38873  itgsbtaddcnst  38874  dirkeritg  38995  dirkercncflem2  38997  fourierdlem28  39028  fourierdlem39  39039  fourierdlem56  39055  fourierdlem57  39056  fourierdlem58  39057  fourierdlem59  39058  fourierdlem60  39059  fourierdlem61  39060  fourierdlem62  39061  fourierdlem68  39067  fourierdlem72  39071  fouriersw  39124  etransclem2  39129  etransclem23  39150  etransclem35  39162  etransclem38  39165  etransclem39  39166  etransclem44  39171  etransclem45  39172  etransclem46  39173  etransclem47  39174