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  5593  mpteqb  5725  chfnrn  5746  dffo5  5784  ffvresb  5798  fmptcof  5802  dfmptg  5814  mpo2eqb  6114  ralrnmpo  6119  rexrnmpo  6120  uchoice  6283  fnmpo  6348  mpoexxg  6356  smores  6438  riinerm  6755  ixpm  6877  difinfinf  7268  nninfwlpoimlemginf  7343  exmidontriimlem1  7403  onntri13  7423  onntri24  7427  cc4f  7455  cc4n  7457  cauappcvgprlemdisj  7838  caucvgsrlemasr  7977  caucvgsr  7989  suplocsr  7996  rexuz3  11501  recvguniq  11506  cau3lem  11625  caubnd2  11628  rexanre  11731  climi2  11799  climi0  11800  climcaucn  11862  ndvdssub  12441  gcdsupex  12478  gcdsupcl  12479  bezoutlemmo  12527  ptex  13297  mgmidmo  13405  issubg2m  13726  eltg2b  14728  neipsm  14828  lmcvg  14891  txlm  14953  metrest  15180  mulcncflem  15281  wlkvtxeledgg  16055  upgrwlkcompim  16073  upgrwlkvtxedg  16075  bj-charfunbi  16174  bj-indint  16294  bj-indind  16295  bj-bdfindis  16310  setindis  16330  bdsetindis  16332  neap0mkv  16437