Theorem ralimi 2557

Description: Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)

Hypothesis

Ref	Expression
ralimi.1	|- ( ph -> ps )

Assertion

Ref	Expression
ralimi	|- ( A. x e. A ph -> A. x e. A ps )

Proof of Theorem ralimi

Step	Hyp	Ref	Expression
1		ralimi.1	. . 3 |- ( ph -> ps )
2	1	a1i 9	. 2 |- ( x e. A -> ( ph -> ps ) )
3	2	ralimia 2555	1 |- ( A. x e. A ph -> A. x e. A ps )

Syntax hints:   -> wi 4   e. wcel 2164   A.wral 2472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460

This theorem depends on definitions:  df-bi 117  df-ral 2477

This theorem is referenced by:  2ralimi  2558  ral2imi  2559  r19.26  2620  r19.29  2631  rr19.3v  2899  rr19.28v  2900  reu3  2950  uniiunlem  3268  reupick2  3445  uniss2  3866  ss2iun  3927  iineq2  3929  iunss2  3957  disjss2  4009  disjeq2  4010  disjnim  4020  repizf  4145  abnexg  4477  reusv3i  4490  tfis  4615  ssrel2  4749  issref  5048  dmmptg  5163  funco  5294  fununi  5322  fun11uni  5324  funimaexglem  5337  fnmpt  5380  fun11iun  5521  mpteqb  5648  chfnrn  5669  dffo5  5707  ffvresb  5721  fmptcof  5725  dfmptg  5737  mpo2eqb  6028  ralrnmpo  6033  rexrnmpo  6034  uchoice  6190  fnmpo  6255  mpoexxg  6263  smores  6345  riinerm  6662  ixpm  6784  difinfinf  7160  nninfwlpoimlemginf  7235  exmidontriimlem1  7281  onntri13  7298  onntri24  7302  cc4f  7329  cc4n  7331  cauappcvgprlemdisj  7711  caucvgsrlemasr  7850  caucvgsr  7862  suplocsr  7869  rexuz3  11134  recvguniq  11139  cau3lem  11258  caubnd2  11261  rexanre  11364  climi2  11431  climi0  11432  climcaucn  11494  ndvdssub  12071  gcdsupex  12094  gcdsupcl  12095  bezoutlemmo  12143  ptex  12875  mgmidmo  12955  issubg2m  13259  eltg2b  14222  neipsm  14322  lmcvg  14385  txlm  14447  metrest  14674  mulcncflem  14761  bj-charfunbi  15303  bj-indint  15423  bj-indind  15424  bj-bdfindis  15439  setindis  15459  bdsetindis  15461  neap0mkv  15559