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

Theorem ralrimi 2789
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 1782 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  ps ) )
4 df-ral 2712 . 2  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
53, 4sylibr 205 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1550   F/wnf 1554    e. wcel 1726   A.wral 2707
This theorem is referenced by:  ralrimiv  2790  reximdai  2816  r19.12  2821  rexlimd  2829  rexlimd2  2830  r19.29af2  2850  r19.37  2859  ralcom2  2874  2rmorex  3140  iineq2d  4115  disjxiun  4211  mpteq2da  4296  reusv6OLD  4736  mpteqb  5821  zfrep6  5970  eusvobj2  6584  riotasv3dOLD  6601  tfr3  6662  tz7.49  6704  mapxpen  7275  dfac2  8013  hsmexlem4  8311  axcc3  8320  domtriomlem  8324  axdc3lem2  8333  axdc3lem4  8335  axdc4lem  8337  ac6num  8361  mreexexd  13875  ptcnplem  17655  xkocnv  17848  cfilucfilOLD  18601  cfilucfil  18602  itg2splitlem  19642  itg2split  19643  itgeq1f  19665  funimass4f  24046  fcomptf  24079  offval2f  24082  funcnvmptOLD  24084  funcnvmpt  24085  esumeq12dvaf  24430  esumel  24444  esumf1o  24447  esumc  24448  esummono  24452  esumlef  24456  esumfsup  24462  esumpinfval  24465  esumpinfsum  24469  measinblem  24576  voliune  24587  volmeas  24589  dstrvprob  24731  untsucf  25161  dedekind  25189  dedekindle  25190  trpredmintr  25511  wfrlem4  25543  frrlem4  25587  mptelee  25836  cover2  26417  upixp  26433  indexdom  26438  filbcmb  26444  sdclem2  26448  eq0rabdioph  26837  eqrabdioph  26838  setindtr  27097  rzalf  27666  fnchoice  27678  refsumcn  27679  rfcnnnub  27685  refsum2cnlem1  27686  fmptdf  27696  climsuse  27712  stoweidlem5  27732  stoweidlem16  27743  stoweidlem18  27745  stoweidlem21  27748  stoweidlem26  27753  stoweidlem27  27754  stoweidlem28  27755  stoweidlem29  27756  stoweidlem31  27758  stoweidlem34  27761  stoweidlem36  27763  stoweidlem41  27768  stoweidlem42  27769  stoweidlem44  27771  stoweidlem45  27772  stoweidlem48  27775  stoweidlem51  27778  stoweidlem52  27779  stoweidlem55  27782  stoweidlem59  27786  stoweidlem60  27787  stoweidlem62  27789  wallispilem3  27794  stirlinglem5  27805  iunconlem2  29049  bnj1379  29204  bnj1145  29364  bnj1204  29383  bnj1388  29404  bnj1417  29412  bnj1489  29427
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-nf 1555  df-ral 2712
  Copyright terms: Public domain W3C validator