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  rzalf  26855  fsumcnf  26859  fnchoice  26867  refsumcn  26868  rfcnnnub  26874  refsum2cnlem1  26875  stoweidlem5  26888  stoweidlem16  26899  stoweidlem17  26900  stoweidlem18  26901  stoweidlem19  26902  stoweidlem21  26904  stoweidlem26  26909  stoweidlem27  26910  stoweidlem28  26911  stoweidlem29  26912  stoweidlem31  26914  stoweidlem34  26917  stoweidlem35  26918  stoweidlem36  26919  stoweidlem41  26924  stoweidlem42  26925  stoweidlem44  26927  stoweidlem45  26928  stoweidlem48  26931  stoweidlem51  26934  stoweidlem52  26935  stoweidlem55  26938  stoweidlem59  26942  stoweidlem60  26943  stoweidlem61  26944  stoweidlem62  26945  stoweid  26946  bnj1379  27649  bnj1145  27809  bnj1204  27828  bnj1388  27849  bnj1417  27857  bnj1489  27872
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