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

Theorem ralrimi 2624
Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.)
Hypotheses
Ref Expression
ralrimi.1  |-  F/ x ph
ralrimi.2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
Assertion
Ref Expression
ralrimi  |-  ( ph  ->  A. x  e.  A  ps )

Proof of Theorem ralrimi
StepHypRef Expression
1 ralrimi.1 . . 3  |-  F/ x ph
2 ralrimi.2 . . 3  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
31, 2alrimi 1745 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  ps ) )
4 df-ral 2548 . 2  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
53, 4sylibr 203 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527   F/wnf 1531    e. wcel 1684   A.wral 2543
This theorem is referenced by:  ralrimiv  2625  reximdai  2651  r19.12  2656  rexlimd  2664  rexlimd2  2665  r19.37  2689  ralcom2  2704  2rmorex  2969  iineq2d  3925  disjxiun  4020  mpteq2da  4105  reusv6OLD  4545  mpteqb  5614  zfrep6  5748  eusvobj2  6337  riotasv3dOLD  6354  tfr3  6415  tz7.49  6457  mapxpen  7027  dfac2  7757  hsmexlem4  8055  axcc3  8064  domtriomlem  8068  axdc3lem2  8077  axdc3lem4  8079  axdc4lem  8081  ac6num  8106  zindd  10113  mreexexd  13550  ptcnplem  17315  xkocnv  17505  itg2splitlem  19103  itg2split  19104  itgeq1f  19126  funimass4f  23042  fmptdF  23221  fcomptf  23230  offval2f  23233  funcnvmptOLD  23234  funcnvmpt  23235  isoun  23242  esumeq12dvaf  23414  esumel  23426  esumf1o  23429  esumc  23430  esumlef  23435  esumpinfval  23441  esumpinfsum  23445  measinblem  23547  dstrvprob  23672  untsucf  24056  dedekind  24082  dedekindle  24083  trpredmintr  24234  wfrlem4  24259  frrlem4  24284  mptelee  24523  svli2  25484  cmpmon  25815  cover2  26358  upixp  26403  indexdom  26413  filbcmb  26432  sdclem2  26452  eq0rabdioph  26856  eqrabdioph  26857  setindtr  27117  rzalf  27688  fsumcnf  27692  fnchoice  27700  refsumcn  27701  rfcnnnub  27707  refsum2cnlem1  27708  fmptdf  27718  clim1fr1  27727  climsuse  27734  stoweidlem5  27754  stoweidlem16  27765  stoweidlem17  27766  stoweidlem18  27767  stoweidlem19  27768  stoweidlem21  27770  stoweidlem26  27775  stoweidlem27  27776  stoweidlem28  27777  stoweidlem29  27778  stoweidlem31  27780  stoweidlem34  27783  stoweidlem35  27784  stoweidlem36  27785  stoweidlem41  27790  stoweidlem42  27791  stoweidlem44  27793  stoweidlem45  27794  stoweidlem48  27797  stoweidlem51  27800  stoweidlem52  27801  stoweidlem55  27804  stoweidlem59  27808  stoweidlem60  27809  stoweidlem61  27810  stoweidlem62  27811  stoweid  27812  wallispilem3  27816  stirlinglem5  27827  stirlinglem13  27835  bnj1379  28863  bnj1145  29023  bnj1204  29042  bnj1388  29063  bnj1417  29071  bnj1489  29086
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-nf 1532  df-ral 2548
  Copyright terms: Public domain W3C validator