Theorem reelprrecn 11136

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

Syntax hints:   ∈ wcel 2109  {cpr 4587  ℂcc 11042  ℝcr 11043

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-cnex 11100  ax-resscn 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-un 3916  df-in 3918  df-ss 3928  df-sn 4586  df-pr 4588

This theorem is referenced by:  dvf  25784  dvmptresicc  25793  dvmptcj  25848  dvmptre  25849  dvmptim  25850  rolle  25870  cmvth  25871  cmvthOLD  25872  mvth  25873  dvlip  25874  dvlipcn  25875  dvle  25888  dvivthlem1  25889  dvivth  25891  lhop2  25896  dvcnvre  25900  dvfsumle  25902  dvfsumleOLD  25903  dvfsumge  25904  dvfsumabs  25905  dvfsumlem2  25909  dvfsumlem2OLD  25910  dvfsum2  25917  ftc2  25927  itgparts  25930  itgsubstlem  25931  itgpowd  25933  aalioulem3  26218  taylthlem2  26258  taylthlem2OLD  26259  taylth  26260  efcvx  26335  pige3ALT  26405  dvrelog  26522  advlog  26539  advlogexp  26540  logccv  26548  dvcxp1  26625  loglesqrt  26647  divsqrtsumlem  26866  lgamgulmlem2  26916  logexprlim  27112  logdivsum  27420  log2sumbnd  27431  fdvneggt  34564  fdvnegge  34566  itgexpif  34570  logdivsqrle  34614  ftc2nc  37669  dvreasin  37673  dvreacos  37674  areacirclem1  37675  dvrelog2  42025  dvrelog3  42026  dvrelog2b  42027  dvrelogpow2b  42029  aks4d1p1p6  42034  redvmptabs  42321  readvrec2  42322  readvrec  42323  readvcot  42325  lhe4.4ex1a  44291  dvcosre  45883  dvcnre  45887  itgsin0pilem1  45921  itgsinexplem1  45925  itgcoscmulx  45940  itgiccshift  45951  itgperiod  45952  itgsbtaddcnst  45953  dirkeritg  46073  dirkercncflem2  46075  fourierdlem28  46106  fourierdlem39  46117  fourierdlem56  46133  fourierdlem57  46134  fourierdlem58  46135  fourierdlem59  46136  fourierdlem60  46137  fourierdlem61  46138  fourierdlem62  46139  fourierdlem68  46145  fourierdlem72  46149  fouriersw  46202  etransclem2  46207  etransclem23  46228  etransclem35  46240  etransclem38  46243  etransclem39  46244  etransclem44  46249  etransclem45  46250  etransclem46  46251  etransclem47  46252