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

Theorem ralrimi 2599
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 1706 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  ps ) )
4 df-ral 2523 . 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 6   A.wal 1532   F/wnf 1539    e. wcel 1621   A.wral 2518
This theorem is referenced by:  ralrimiv  2600  reximdai  2626  r19.12  2631  rexlimd  2639  rexlimd2  2640  r19.37  2664  ralcom2  2679  2rmorex  2944  iineq2d  3899  disjxiun  3994  mpteq2da  4079  reusv6OLD  4517  mpteqb  5548  zfrep6  5682  eusvobj2  6305  riotasv3dOLD  6322  tfr3  6383  tz7.49  6425  mapxpen  6995  dfac2  7725  hsmexlem4  8023  axcc3  8032  domtriomlem  8036  axdc3lem2  8045  axdc3lem4  8047  axdc4lem  8049  ac6num  8074  zindd  10080  mreexexd  13512  ptcnplem  17277  xkocnv  17467  itg2splitlem  19065  itg2split  19066  itgeq1f  19088  funimass4f  23003  untsucf  23428  dedekind  23453  dedekindle  23454  trpredmintr  23603  wfrlem4  23628  frrlem4  23653  mptelee  23898  svli2  24851  cmpmon  25182  cover2  25725  upixp  25770  indexdom  25780  filbcmb  25799  sdclem2  25819  eq0rabdioph  26223  eqrabdioph  26224  setindtr  26484  rzalf  27056  fsumcnf  27060  fnchoice  27068  refsumcn  27069  rfcnnnub  27075  refsum2cnlem1  27076  stoweidlem5  27089  stoweidlem16  27100  stoweidlem17  27101  stoweidlem18  27102  stoweidlem19  27103  stoweidlem21  27105  stoweidlem26  27110  stoweidlem27  27111  stoweidlem28  27112  stoweidlem29  27113  stoweidlem31  27115  stoweidlem34  27118  stoweidlem35  27119  stoweidlem36  27120  stoweidlem41  27125  stoweidlem42  27126  stoweidlem44  27128  stoweidlem45  27129  stoweidlem48  27132  stoweidlem51  27135  stoweidlem52  27136  stoweidlem55  27139  stoweidlem59  27143  stoweidlem60  27144  stoweidlem61  27145  stoweidlem62  27146  stoweid  27147  bnj1379  27912  bnj1145  28072  bnj1204  28091  bnj1388  28112  bnj1417  28120  bnj1489  28135
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-nf 1540  df-ral 2523
  Copyright terms: Public domain W3C validator