Theorem ralimi 2595

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

Syntax hints:   -> wi 4   e. wcel 2202   A.wral 2510

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

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

This theorem is referenced by:  2ralimi  2596  ral2imi  2597  r19.26  2659  r19.29  2670  rr19.3v  2945  rr19.28v  2946  reu3  2996  uniiunlem  3316  reupick2  3493  uniss2  3924  ss2iun  3985  iineq2  3987  iunss2  4015  disjss2  4067  disjeq2  4068  disjnim  4078  repizf  4205  abnexg  4543  reusv3i  4556  tfis  4681  ssrel2  4816  issref  5119  dmmptg  5234  funco  5366  fununi  5398  fun11uni  5400  funimaexglem  5413  fnmpt  5459  fun11iun  5604  mpteqb  5737  chfnrn  5758  dffo5  5796  ffvresb  5810  fmptcof  5814  dfmptg  5827  mpo2eqb  6131  ralrnmpo  6136  rexrnmpo  6137  uchoice  6300  fnmpo  6367  mpoexxg  6375  smores  6458  riinerm  6777  ixpm  6899  difinfinf  7300  nninfwlpoimlemginf  7375  exmidontriimlem1  7436  onntri13  7456  onntri24  7460  cc4f  7488  cc4n  7490  cauappcvgprlemdisj  7871  caucvgsrlemasr  8010  caucvgsr  8022  suplocsr  8029  rexuz3  11568  recvguniq  11573  cau3lem  11692  caubnd2  11695  rexanre  11798  climi2  11866  climi0  11867  climcaucn  11929  ndvdssub  12509  gcdsupex  12546  gcdsupcl  12547  bezoutlemmo  12595  ptex  13365  mgmidmo  13473  issubg2m  13794  eltg2b  14797  neipsm  14897  lmcvg  14960  txlm  15022  metrest  15249  mulcncflem  15350  wlkvtxeledgg  16214  upgrwlkcompim  16232  upgrwlkvtxedg  16234  upgr2wlkdc  16247  bj-charfunbi  16457  bj-indint  16577  bj-indind  16578  bj-bdfindis  16593  setindis  16613  bdsetindis  16615  pw1dceq  16656  neap0mkv  16725