Theorem ralimi 2426

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

Syntax hints:   -> wi 4   e. wcel 1433   A.wral 2348

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378

This theorem depends on definitions:  df-bi 115  df-ral 2353

This theorem is referenced by:  ral2imi  2427  r19.26  2485  r19.29  2494  rr19.3v  2733  rr19.28v  2734  reu3  2782  uniiunlem  3082  reupick2  3250  uniss2  3632  ss2iun  3693  iineq2  3695  iunss2  3723  disjss2  3769  disjeq2  3770  repizf  3894  reusv3i  4209  tfis  4324  ssrel2  4448  issref  4727  dmmptg  4838  funco  4960  fununi  4987  fun11uni  4989  funimaexglem  5002  fnmpt  5045  fun11iun  5167  mpteqb  5282  chfnrn  5299  dffo5  5337  ffvresb  5349  fmptcof  5352  dfmptg  5363  mpt22eqb  5630  ralrnmpt2  5635  rexrnmpt2  5636  fnmpt2  5848  mpt2exxg  5853  smores  5930  riinerm  6202  cauappcvgprlemdisj  6841  caucvgsrlemasr  6966  caucvgsr  6978  rexuz3  9876  recvguniq  9881  cau3lem  10000  caubnd2  10003  rexanre  10106  climi2  10127  climi0  10128  climcaucn  10188  ndvdssub  10330  gcdsupex  10349  gcdsupcl  10350  bezoutlemmo  10395  bj-indint  10726  bj-indind  10727  bj-bdfindis  10742  setindis  10762  bdsetindis  10764