MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reelprrecn Structured version   Visualization version   GIF version

Theorem reelprrecn 10621
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
StepHypRef Expression
1 reex 10620 . 2 ℝ ∈ V
21prid1 4696 1 ℝ ∈ {ℝ, ℂ}
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  {cpr 4565  cc 10527  cr 10528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-sep 5199  ax-cnex 10585  ax-resscn 10586
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-rab 3151  df-v 3501  df-un 3944  df-in 3946  df-ss 3955  df-sn 4564  df-pr 4566
This theorem is referenced by:  dvf  24423  dvmptcj  24483  dvmptre  24484  dvmptim  24485  rolle  24505  cmvth  24506  mvth  24507  dvlip  24508  dvlipcn  24509  dvle  24522  dvivthlem1  24523  dvivth  24525  lhop2  24530  dvcnvre  24534  dvfsumle  24536  dvfsumge  24537  dvfsumabs  24538  dvfsumlem2  24542  dvfsum2  24549  ftc2  24559  itgparts  24562  itgsubstlem  24563  aalioulem3  24841  taylthlem2  24880  taylth  24881  efcvx  24955  pige3ALT  25023  dvrelog  25136  advlog  25153  advlogexp  25154  logccv  25162  dvcxp1  25237  loglesqrt  25255  divsqrtsumlem  25474  lgamgulmlem2  25524  logexprlim  25718  logdivsum  26026  log2sumbnd  26037  fdvneggt  31760  fdvnegge  31762  itgexpif  31766  logdivsqrle  31810  ftc2nc  34846  dvreasin  34850  dvreacos  34851  areacirclem1  34852  itgpowd  39689  lhe4.4ex1a  40529  dvcosre  42064  dvcnre  42068  dvmptresicc  42072  itgsin0pilem1  42103  itgsinexplem1  42107  itgcoscmulx  42122  itgiccshift  42133  itgperiod  42134  itgsbtaddcnst  42135  dirkeritg  42256  dirkercncflem2  42258  fourierdlem28  42289  fourierdlem39  42300  fourierdlem56  42316  fourierdlem57  42317  fourierdlem58  42318  fourierdlem59  42319  fourierdlem60  42320  fourierdlem61  42321  fourierdlem62  42322  fourierdlem68  42328  fourierdlem72  42332  fouriersw  42385  etransclem2  42390  etransclem23  42411  etransclem35  42423  etransclem38  42426  etransclem39  42427  etransclem44  42432  etransclem45  42433  etransclem46  42434  etransclem47  42435
  Copyright terms: Public domain W3C validator