Theorem ralimi 2571

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

Syntax hints:   -> wi 4   e. wcel 2178   A.wral 2486

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 1471  ax-gen 1473

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

This theorem is referenced by:  2ralimi  2572  ral2imi  2573  r19.26  2634  r19.29  2645  rr19.3v  2919  rr19.28v  2920  reu3  2970  uniiunlem  3290  reupick2  3467  uniss2  3895  ss2iun  3956  iineq2  3958  iunss2  3986  disjss2  4038  disjeq2  4039  disjnim  4049  repizf  4176  abnexg  4511  reusv3i  4524  tfis  4649  ssrel2  4783  issref  5084  dmmptg  5199  funco  5330  fununi  5361  fun11uni  5363  funimaexglem  5376  fnmpt  5422  fun11iun  5565  mpteqb  5693  chfnrn  5714  dffo5  5752  ffvresb  5766  fmptcof  5770  dfmptg  5782  mpo2eqb  6078  ralrnmpo  6083  rexrnmpo  6084  uchoice  6246  fnmpo  6311  mpoexxg  6319  smores  6401  riinerm  6718  ixpm  6840  difinfinf  7229  nninfwlpoimlemginf  7304  exmidontriimlem1  7364  onntri13  7384  onntri24  7388  cc4f  7416  cc4n  7418  cauappcvgprlemdisj  7799  caucvgsrlemasr  7938  caucvgsr  7950  suplocsr  7957  rexuz3  11416  recvguniq  11421  cau3lem  11540  caubnd2  11543  rexanre  11646  climi2  11714  climi0  11715  climcaucn  11777  ndvdssub  12356  gcdsupex  12393  gcdsupcl  12394  bezoutlemmo  12442  ptex  13211  mgmidmo  13319  issubg2m  13640  eltg2b  14641  neipsm  14741  lmcvg  14804  txlm  14866  metrest  15093  mulcncflem  15194  bj-charfunbi  15946  bj-indint  16066  bj-indind  16067  bj-bdfindis  16082  setindis  16102  bdsetindis  16104  neap0mkv  16210