Theorem reelprrecn 11247

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

Syntax hints:   ∈ wcel 2108  {cpr 4628  ℂcc 11153  ℝcr 11154

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-cnex 11211  ax-resscn 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-un 3956  df-in 3958  df-ss 3968  df-sn 4627  df-pr 4629

This theorem is referenced by:  dvf  25942  dvmptresicc  25951  dvmptcj  26006  dvmptre  26007  dvmptim  26008  rolle  26028  cmvth  26029  cmvthOLD  26030  mvth  26031  dvlip  26032  dvlipcn  26033  dvle  26046  dvivthlem1  26047  dvivth  26049  lhop2  26054  dvcnvre  26058  dvfsumle  26060  dvfsumleOLD  26061  dvfsumge  26062  dvfsumabs  26063  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsum2  26075  ftc2  26085  itgparts  26088  itgsubstlem  26089  itgpowd  26091  aalioulem3  26376  taylthlem2  26416  taylthlem2OLD  26417  taylth  26418  efcvx  26493  pige3ALT  26562  dvrelog  26679  advlog  26696  advlogexp  26697  logccv  26705  dvcxp1  26782  loglesqrt  26804  divsqrtsumlem  27023  lgamgulmlem2  27073  logexprlim  27269  logdivsum  27577  log2sumbnd  27588  fdvneggt  34615  fdvnegge  34617  itgexpif  34621  logdivsqrle  34665  ftc2nc  37709  dvreasin  37713  dvreacos  37714  areacirclem1  37715  dvrelog2  42065  dvrelog3  42066  dvrelog2b  42067  dvrelogpow2b  42069  aks4d1p1p6  42074  redvmptabs  42390  readvrec2  42391  readvrec  42392  readvcot  42394  lhe4.4ex1a  44348  dvcosre  45927  dvcnre  45931  itgsin0pilem1  45965  itgsinexplem1  45969  itgcoscmulx  45984  itgiccshift  45995  itgperiod  45996  itgsbtaddcnst  45997  dirkeritg  46117  dirkercncflem2  46119  fourierdlem28  46150  fourierdlem39  46161  fourierdlem56  46177  fourierdlem57  46178  fourierdlem58  46179  fourierdlem59  46180  fourierdlem60  46181  fourierdlem61  46182  fourierdlem62  46183  fourierdlem68  46189  fourierdlem72  46193  fouriersw  46246  etransclem2  46251  etransclem23  46272  etransclem35  46284  etransclem38  46287  etransclem39  46288  etransclem44  46293  etransclem45  46294  etransclem46  46295  etransclem47  46296