Theorem reelprrecn 11124

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

Syntax hints:   ∈ wcel 2114  {cpr 4570  ℂcc 11030  ℝcr 11031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-cnex 11088  ax-resscn 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-un 3895  df-in 3897  df-ss 3907  df-sn 4569  df-pr 4571

This theorem is referenced by:  dvf  25887  dvmptresicc  25896  dvmptcj  25948  dvmptre  25949  dvmptim  25950  rolle  25970  cmvth  25971  mvth  25972  dvlip  25973  dvlipcn  25974  dvle  25987  dvivthlem1  25988  dvivth  25990  lhop2  25995  dvcnvre  25999  dvfsumle  26001  dvfsumge  26002  dvfsumabs  26003  dvfsumlem2  26007  dvfsum2  26014  ftc2  26024  itgparts  26027  itgsubstlem  26028  itgpowd  26030  aalioulem3  26314  taylthlem2  26354  taylthlem2OLD  26355  taylth  26356  efcvx  26430  pige3ALT  26500  dvrelog  26617  advlog  26634  advlogexp  26635  logccv  26643  dvcxp1  26720  loglesqrt  26741  divsqrtsumlem  26960  lgamgulmlem2  27010  logexprlim  27205  logdivsum  27513  log2sumbnd  27524  fdvneggt  34763  fdvnegge  34765  itgexpif  34769  logdivsqrle  34813  ftc2nc  38040  dvreasin  38044  dvreacos  38045  areacirclem1  38046  dvrelog2  42520  dvrelog3  42521  dvrelog2b  42522  dvrelogpow2b  42524  aks4d1p1p6  42529  redvmptabs  42809  readvrec2  42810  readvrec  42811  readvcot  42813  lhe4.4ex1a  44777  dvcosre  46361  dvcnre  46365  itgsin0pilem1  46399  itgsinexplem1  46403  itgcoscmulx  46418  itgiccshift  46429  itgperiod  46430  itgsbtaddcnst  46431  dirkeritg  46551  dirkercncflem2  46553  fourierdlem28  46584  fourierdlem39  46595  fourierdlem56  46611  fourierdlem57  46612  fourierdlem58  46613  fourierdlem59  46614  fourierdlem60  46615  fourierdlem61  46616  fourierdlem62  46617  fourierdlem68  46623  fourierdlem72  46627  fouriersw  46680  etransclem2  46685  etransclem23  46706  etransclem35  46718  etransclem38  46721  etransclem39  46722  etransclem44  46727  etransclem45  46728  etransclem46  46729  etransclem47  46730