Theorem ralimi 2560

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

Syntax hints:   -> wi 4   e. wcel 2167   A.wral 2475

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 1461  ax-gen 1463

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

This theorem is referenced by:  2ralimi  2561  ral2imi  2562  r19.26  2623  r19.29  2634  rr19.3v  2903  rr19.28v  2904  reu3  2954  uniiunlem  3273  reupick2  3450  uniss2  3871  ss2iun  3932  iineq2  3934  iunss2  3962  disjss2  4014  disjeq2  4015  disjnim  4025  repizf  4150  abnexg  4482  reusv3i  4495  tfis  4620  ssrel2  4754  issref  5053  dmmptg  5168  funco  5299  fununi  5327  fun11uni  5329  funimaexglem  5342  fnmpt  5387  fun11iun  5528  mpteqb  5655  chfnrn  5676  dffo5  5714  ffvresb  5728  fmptcof  5732  dfmptg  5744  mpo2eqb  6036  ralrnmpo  6041  rexrnmpo  6042  uchoice  6204  fnmpo  6269  mpoexxg  6277  smores  6359  riinerm  6676  ixpm  6798  difinfinf  7176  nninfwlpoimlemginf  7251  exmidontriimlem1  7304  onntri13  7321  onntri24  7325  cc4f  7352  cc4n  7354  cauappcvgprlemdisj  7735  caucvgsrlemasr  7874  caucvgsr  7886  suplocsr  7893  rexuz3  11172  recvguniq  11177  cau3lem  11296  caubnd2  11299  rexanre  11402  climi2  11470  climi0  11471  climcaucn  11533  ndvdssub  12112  gcdsupex  12149  gcdsupcl  12150  bezoutlemmo  12198  ptex  12966  mgmidmo  13074  issubg2m  13395  eltg2b  14374  neipsm  14474  lmcvg  14537  txlm  14599  metrest  14826  mulcncflem  14927  bj-charfunbi  15541  bj-indint  15661  bj-indind  15662  bj-bdfindis  15677  setindis  15697  bdsetindis  15699  neap0mkv  15800