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

Theorem ralrimi 2626
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 1747 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  ps ) )
4 df-ral 2550 . 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 1528   F/wnf 1532    e. wcel 1685   A.wral 2545
This theorem is referenced by:  ralrimiv  2627  reximdai  2653  r19.12  2658  rexlimd  2666  rexlimd2  2667  r19.37  2691  ralcom2  2706  2rmorex  2971  iineq2d  3927  disjxiun  4022  mpteq2da  4107  reusv6OLD  4545  mpteqb  5576  zfrep6  5710  eusvobj2  6333  riotasv3dOLD  6350  tfr3  6411  tz7.49  6453  mapxpen  7023  dfac2  7753  hsmexlem4  8051  axcc3  8060  domtriomlem  8064  axdc3lem2  8073  axdc3lem4  8075  axdc4lem  8077  ac6num  8102  zindd  10109  mreexexd  13545  ptcnplem  17310  xkocnv  17500  itg2splitlem  19098  itg2split  19099  itgeq1f  19121  funimass4f  23036  untsucf  23461  dedekind  23486  dedekindle  23487  trpredmintr  23636  wfrlem4  23661  frrlem4  23686  mptelee  23931  svli2  24884  cmpmon  25215  cover2  25758  upixp  25803  indexdom  25813  filbcmb  25832  sdclem2  25852  eq0rabdioph  26256  eqrabdioph  26257  setindtr  26517  rzalf  27088  fsumcnf  27092  fnchoice  27100  refsumcn  27101  rfcnnnub  27107  refsum2cnlem1  27108  fmptdf  27118  clim1fr1  27127  climsuse  27134  stoweidlem5  27154  stoweidlem16  27165  stoweidlem17  27166  stoweidlem18  27167  stoweidlem19  27168  stoweidlem21  27170  stoweidlem26  27175  stoweidlem27  27176  stoweidlem28  27177  stoweidlem29  27178  stoweidlem31  27180  stoweidlem34  27183  stoweidlem35  27184  stoweidlem36  27185  stoweidlem41  27190  stoweidlem42  27191  stoweidlem44  27193  stoweidlem45  27194  stoweidlem48  27197  stoweidlem51  27200  stoweidlem52  27201  stoweidlem55  27204  stoweidlem59  27208  stoweidlem60  27209  stoweidlem61  27210  stoweidlem62  27211  stoweid  27212  wallispilem3  27216  stirlinglem5  27227  stirlinglem13  27235  bnj1379  28131  bnj1145  28291  bnj1204  28310  bnj1388  28331  bnj1417  28339  bnj1489  28354
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-11 1716
This theorem depends on definitions:  df-bi 179  df-nf 1533  df-ral 2550
  Copyright terms: Public domain W3C validator