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

Theorem ralrimi 2586
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 2513 . 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 2509
This theorem is referenced by:  ralrimiv  2587  reximdai  2613  r19.12  2618  rexlimd  2626  rexlimd2  2627  r19.37  2651  ralcom2  2666  iineq2d  3823  disjxiun  3917  mpteq2da  4002  reusv6OLD  4436  mpteqb  5466  zfrep6  5600  eusvobj2  6223  riotasv3dOLD  6240  tfr3  6301  tz7.49  6343  mapxpen  6912  dfac2  7641  hsmexlem4  7939  axcc3  7948  domtriomlem  7952  axdc3lem2  7961  axdc3lem4  7963  axdc4lem  7965  ac6num  7990  zindd  9992  ptcnplem  17147  xkocnv  17337  itg2splitlem  18935  itg2split  18936  itgeq1f  18958  untsucf  23227  dedekind  23252  dedekindle  23253  trpredmintr  23402  wfrlem4  23427  frrlem4  23452  mptelee  23697  svli2  24650  cmpmon  24981  cover2  25524  upixp  25569  indexdom  25579  filbcmb  25598  sdclem2  25618  eq0rabdioph  26022  eqrabdioph  26023  setindtr  26283  bnj1379  27552  bnj1145  27712  bnj1204  27731  bnj1388  27752  bnj1417  27760  bnj1489  27775
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 2513
  Copyright terms: Public domain W3C validator