Theorem ralimi 2593

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

Syntax hints:   -> wi 4   e. wcel 2200   A.wral 2508

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 1493  ax-gen 1495

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

This theorem is referenced by:  2ralimi  2594  ral2imi  2595  r19.26  2657  r19.29  2668  rr19.3v  2942  rr19.28v  2943  reu3  2993  uniiunlem  3313  reupick2  3490  uniss2  3919  ss2iun  3980  iineq2  3982  iunss2  4010  disjss2  4062  disjeq2  4063  disjnim  4073  repizf  4200  abnexg  4537  reusv3i  4550  tfis  4675  ssrel2  4809  issref  5111  dmmptg  5226  funco  5358  fununi  5389  fun11uni  5391  funimaexglem  5404  fnmpt  5450  fun11iun  5595  mpteqb  5727  chfnrn  5748  dffo5  5786  ffvresb  5800  fmptcof  5804  dfmptg  5816  mpo2eqb  6120  ralrnmpo  6125  rexrnmpo  6126  uchoice  6289  fnmpo  6354  mpoexxg  6362  smores  6444  riinerm  6763  ixpm  6885  difinfinf  7279  nninfwlpoimlemginf  7354  exmidontriimlem1  7414  onntri13  7434  onntri24  7438  cc4f  7466  cc4n  7468  cauappcvgprlemdisj  7849  caucvgsrlemasr  7988  caucvgsr  8000  suplocsr  8007  rexuz3  11517  recvguniq  11522  cau3lem  11641  caubnd2  11644  rexanre  11747  climi2  11815  climi0  11816  climcaucn  11878  ndvdssub  12457  gcdsupex  12494  gcdsupcl  12495  bezoutlemmo  12543  ptex  13313  mgmidmo  13421  issubg2m  13742  eltg2b  14744  neipsm  14844  lmcvg  14907  txlm  14969  metrest  15196  mulcncflem  15297  wlkvtxeledgg  16090  upgrwlkcompim  16108  upgrwlkvtxedg  16110  upgr2wlkdc  16121  bj-charfunbi  16257  bj-indint  16377  bj-indind  16378  bj-bdfindis  16393  setindis  16413  bdsetindis  16415  pw1dceq  16457  neap0mkv  16525