Theorem ralimi 2569

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

Syntax hints:   -> wi 4   e. wcel 2176   A.wral 2484

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 1470  ax-gen 1472

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

This theorem is referenced by:  2ralimi  2570  ral2imi  2571  r19.26  2632  r19.29  2643  rr19.3v  2912  rr19.28v  2913  reu3  2963  uniiunlem  3282  reupick2  3459  uniss2  3881  ss2iun  3942  iineq2  3944  iunss2  3972  disjss2  4024  disjeq2  4025  disjnim  4035  repizf  4161  abnexg  4494  reusv3i  4507  tfis  4632  ssrel2  4766  issref  5066  dmmptg  5181  funco  5312  fununi  5343  fun11uni  5345  funimaexglem  5358  fnmpt  5404  fun11iun  5545  mpteqb  5672  chfnrn  5693  dffo5  5731  ffvresb  5745  fmptcof  5749  dfmptg  5761  mpo2eqb  6057  ralrnmpo  6062  rexrnmpo  6063  uchoice  6225  fnmpo  6290  mpoexxg  6298  smores  6380  riinerm  6697  ixpm  6819  difinfinf  7205  nninfwlpoimlemginf  7280  exmidontriimlem1  7335  onntri13  7352  onntri24  7356  cc4f  7383  cc4n  7385  cauappcvgprlemdisj  7766  caucvgsrlemasr  7905  caucvgsr  7917  suplocsr  7924  rexuz3  11334  recvguniq  11339  cau3lem  11458  caubnd2  11461  rexanre  11564  climi2  11632  climi0  11633  climcaucn  11695  ndvdssub  12274  gcdsupex  12311  gcdsupcl  12312  bezoutlemmo  12360  ptex  13129  mgmidmo  13237  issubg2m  13558  eltg2b  14559  neipsm  14659  lmcvg  14722  txlm  14784  metrest  15011  mulcncflem  15112  bj-charfunbi  15784  bj-indint  15904  bj-indind  15905  bj-bdfindis  15920  setindis  15940  bdsetindis  15942  neap0mkv  16045