Theorem ralimi 2540

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

Syntax hints:   -> wi 4   e. wcel 2148   A.wral 2455

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 1447  ax-gen 1449

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

This theorem is referenced by:  2ralimi  2541  ral2imi  2542  r19.26  2603  r19.29  2614  rr19.3v  2878  rr19.28v  2879  reu3  2929  uniiunlem  3246  reupick2  3423  uniss2  3842  ss2iun  3903  iineq2  3905  iunss2  3933  disjss2  3985  disjeq2  3986  disjnim  3996  repizf  4121  abnexg  4448  reusv3i  4461  tfis  4584  ssrel2  4718  issref  5013  dmmptg  5128  funco  5258  fununi  5286  fun11uni  5288  funimaexglem  5301  fnmpt  5344  fun11iun  5484  mpteqb  5608  chfnrn  5629  dffo5  5667  ffvresb  5681  fmptcof  5685  dfmptg  5697  mpo2eqb  5986  ralrnmpo  5991  rexrnmpo  5992  fnmpo  6205  mpoexxg  6213  smores  6295  riinerm  6610  ixpm  6732  difinfinf  7102  nninfwlpoimlemginf  7176  exmidontriimlem1  7222  onntri13  7239  onntri24  7243  cc4f  7270  cc4n  7272  cauappcvgprlemdisj  7652  caucvgsrlemasr  7791  caucvgsr  7803  suplocsr  7810  rexuz3  11001  recvguniq  11006  cau3lem  11125  caubnd2  11128  rexanre  11231  climi2  11298  climi0  11299  climcaucn  11361  ndvdssub  11937  gcdsupex  11960  gcdsupcl  11961  bezoutlemmo  12009  ptex  12718  mgmidmo  12796  issubg2m  13054  eltg2b  13639  neipsm  13739  lmcvg  13802  txlm  13864  metrest  14091  mulcncflem  14175  bj-charfunbi  14648  bj-indint  14768  bj-indind  14769  bj-bdfindis  14784  setindis  14804  bdsetindis  14806  neap0mkv  14902