Theorem ralimi 2529

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

Syntax hints:   -> wi 4   e. wcel 2136   A.wral 2444

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 1435  ax-gen 1437

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

This theorem is referenced by:  2ralimi  2530  ral2imi  2531  r19.26  2592  r19.29  2603  rr19.3v  2865  rr19.28v  2866  reu3  2916  uniiunlem  3231  reupick2  3408  uniss2  3820  ss2iun  3881  iineq2  3883  iunss2  3911  disjss2  3962  disjeq2  3963  disjnim  3973  repizf  4098  abnexg  4424  reusv3i  4437  tfis  4560  ssrel2  4694  issref  4986  dmmptg  5101  funco  5228  fununi  5256  fun11uni  5258  funimaexglem  5271  fnmpt  5314  fun11iun  5453  mpteqb  5576  chfnrn  5596  dffo5  5634  ffvresb  5648  fmptcof  5652  dfmptg  5664  mpo2eqb  5951  ralrnmpo  5956  rexrnmpo  5957  fnmpo  6170  mpoexxg  6178  smores  6260  riinerm  6574  ixpm  6696  difinfinf  7066  exmidontriimlem1  7177  onntri13  7194  onntri24  7198  cc4f  7210  cc4n  7212  cauappcvgprlemdisj  7592  caucvgsrlemasr  7731  caucvgsr  7743  suplocsr  7750  rexuz3  10932  recvguniq  10937  cau3lem  11056  caubnd2  11059  rexanre  11162  climi2  11229  climi0  11230  climcaucn  11292  ndvdssub  11867  gcdsupex  11890  gcdsupcl  11891  bezoutlemmo  11939  mgmidmo  12603  eltg2b  12694  neipsm  12794  lmcvg  12857  txlm  12919  metrest  13146  mulcncflem  13230  bj-charfunbi  13693  bj-indint  13813  bj-indind  13814  bj-bdfindis  13829  setindis  13849  bdsetindis  13851