MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexri Unicode version

Theorem rexri 9667
Description: A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)
Hypothesis
Ref Expression
rexri.1
Assertion
Ref Expression
rexri

Proof of Theorem rexri
StepHypRef Expression
1 rexri.1 . 2
2 rexr 9660 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818   cr 9512   cxr 9648
This theorem is referenced by:  xmulid1  11500  xmulid2  11501  xmulm1  11502  x2times  11520  xov1plusxeqvd  11695  hashge1  12457  hashgt12el  12481  hashgt12el2  12482  sgn1  12925  tanhbnd  13896  isnzr2hash  17912  0ringnnzr  17917  xrsnsgrp  18454  leordtval2  19713  nmoid  21249  metnrmlem1a  21362  metnrmlem1  21363  icopnfcnv  21442  icopnfhmeo  21443  iccpnfcnv  21444  iccpnfhmeo  21445  oprpiece1res1  21451  oprpiece1res2  21452  pcoass  21524  vitalilem4  22020  itg2monolem1  22157  itg2monolem3  22159  abelthlem3  22828  abelth  22836  neghalfpirx  22859  sincosq1sgn  22891  sincosq2sgn  22892  sincosq4sgn  22894  coseq00topi  22895  coseq0negpitopi  22896  tanabsge  22899  sinq12gt0  22900  cosq14gt0  22903  cosordlem  22918  tanord1  22924  tanord  22925  tanregt0  22926  negpitopissre  22927  ellogrn  22947  logimclad  22960  argregt0  22995  argimgt0  22997  argimlt0  22998  dvloglem  23029  logf1o2  23031  dvlog2lem  23033  efopnlem2  23038  isosctrlem1  23152  asinneg  23217  asinsinlem  23222  acoscos  23224  reasinsin  23227  atanlogsublem  23246  atantan  23254  atanbndlem  23256  atanbnd  23257  atan1  23259  scvxcvx  23315  dchrvmasumlem2  23683  dchrvmasumiflem1  23686  pntibndlem1  23774  pntibndlem2  23776  pntibnd  23778  pntlemc  23780  pnt  23799  padicabvf  23816  padicabvcxp  23817  tgldimor  23893  umgrafi  24322  vdgfrgragt2  25027  nmopun  26933  nmoptrii  27013  nmopcoi  27014  pjnmopi  27067  xlt2addrd  27578  xdivrec  27623  xrsmulgzz  27666  xrnarchi  27728  unitssxrge0  27882  xrge0iifcnv  27915  xrge0iifiso  27917  xrge0iifhom  27919  hasheuni  28091  ddemeas  28208  prob01  28352  sgnsgn  28487  sin2h  30045  cos2h  30046  tan2h  30047  asindmre  30102  dvasin  30103  dvacos  30104  areacirclem1  30107  areaquad  31184  cvgdvgrat  31194  fprodge1  31598  itgsin0pilem1  31748  fourierdlem24  31913  fourierdlem38  31927  fourierdlem43  31932  fourierdlem44  31933  fourierdlem46  31935  fourierdlem62  31951  fourierdlem74  31963  fourierdlem75  31964  fourierdlem85  31974  fourierdlem88  31977  fourierdlem93  31982  fourierdlem102  31991  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  fourierdlem112  32001  fourierdlem114  32003  sqwvfoura  32011  sqwvfourb  32012  fourierswlem  32013  fouriersw  32014  fouriercn  32015  pgrpgt2nabl  32959  isosctrlem1ALT  33734  sineq0ALT  33737  bj-flbi3  34608  bj-pinftyccb  34624  bj-minftyccb  34628  bj-pinftynminfty  34630  imo72b2  37993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-in 3482  df-ss 3489  df-xr 9653
  Copyright terms: Public domain W3C validator