Theorem ralimi 2533

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 2531	1 |- ( A. x e. A ph -> A. x e. A ps )

Syntax hints:   -> wi 4   e. wcel 2141   A.wral 2448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442

This theorem depends on definitions:  df-bi 116  df-ral 2453

This theorem is referenced by:  2ralimi  2534  ral2imi  2535  r19.26  2596  r19.29  2607  rr19.3v  2869  rr19.28v  2870  reu3  2920  uniiunlem  3236  reupick2  3413  uniss2  3827  ss2iun  3888  iineq2  3890  iunss2  3918  disjss2  3969  disjeq2  3970  disjnim  3980  repizf  4105  abnexg  4431  reusv3i  4444  tfis  4567  ssrel2  4701  issref  4993  dmmptg  5108  funco  5238  fununi  5266  fun11uni  5268  funimaexglem  5281  fnmpt  5324  fun11iun  5463  mpteqb  5586  chfnrn  5607  dffo5  5645  ffvresb  5659  fmptcof  5663  dfmptg  5675  mpo2eqb  5962  ralrnmpo  5967  rexrnmpo  5968  fnmpo  6181  mpoexxg  6189  smores  6271  riinerm  6586  ixpm  6708  difinfinf  7078  nninfwlpoimlemginf  7152  exmidontriimlem1  7198  onntri13  7215  onntri24  7219  cc4f  7231  cc4n  7233  cauappcvgprlemdisj  7613  caucvgsrlemasr  7752  caucvgsr  7764  suplocsr  7771  rexuz3  10954  recvguniq  10959  cau3lem  11078  caubnd2  11081  rexanre  11184  climi2  11251  climi0  11252  climcaucn  11314  ndvdssub  11889  gcdsupex  11912  gcdsupcl  11913  bezoutlemmo  11961  mgmidmo  12626  eltg2b  12848  neipsm  12948  lmcvg  13011  txlm  13073  metrest  13300  mulcncflem  13384  bj-charfunbi  13846  bj-indint  13966  bj-indind  13967  bj-bdfindis  13982  setindis  14002  bdsetindis  14004