Theorem reelprrecn 10234

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

Syntax hints:   ∈ wcel 2145  {cpr 4319  ℂcc 10140  ℝcr 10141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-cnex 10198  ax-resscn 10199

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-un 3728  df-in 3730  df-ss 3737  df-sn 4318  df-pr 4320

This theorem is referenced by:  dvf  23891  dvmptcj  23951  dvmptre  23952  dvmptim  23953  rolle  23973  cmvth  23974  mvth  23975  dvlip  23976  dvlipcn  23977  dvle  23990  dvivthlem1  23991  dvivth  23993  lhop2  23998  dvcnvre  24002  dvfsumle  24004  dvfsumge  24005  dvfsumabs  24006  dvfsumlem2  24010  dvfsum2  24017  ftc2  24027  itgparts  24030  itgsubstlem  24031  aalioulem3  24309  taylthlem2  24348  taylth  24349  efcvx  24423  pige3  24490  dvrelog  24604  advlog  24621  advlogexp  24622  logccv  24630  dvcxp1  24702  loglesqrt  24720  divsqrtsumlem  24927  lgamgulmlem2  24977  logexprlim  25171  logdivsum  25443  log2sumbnd  25454  fdvneggt  31018  fdvnegge  31020  itgexpif  31024  logdivsqrle  31068  ftc2nc  33826  dvreasin  33830  dvreacos  33831  areacirclem1  33832  itgpowd  38326  lhe4.4ex1a  39054  dvcosre  40641  dvcnre  40645  dvmptresicc  40649  itgsin0pilem1  40680  itgsinexplem1  40684  itgcoscmulx  40699  itgiccshift  40710  itgperiod  40711  itgsbtaddcnst  40712  dirkeritg  40833  dirkercncflem2  40835  fourierdlem28  40866  fourierdlem39  40877  fourierdlem56  40893  fourierdlem57  40894  fourierdlem58  40895  fourierdlem59  40896  fourierdlem60  40897  fourierdlem61  40898  fourierdlem62  40899  fourierdlem68  40905  fourierdlem72  40909  fouriersw  40962  etransclem2  40967  etransclem23  40988  etransclem35  41000  etransclem38  41003  etransclem39  41004  etransclem44  41009  etransclem45  41010  etransclem46  41011  etransclem47  41012