Theorem ralimi 2613

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502

This proof depends on definitions:  df-bi 117  df-ral 2533

This theorem is used by:  2ralimi  2614  ral2imi  2615  r19.26  2677  r19.29  2688  rr19.3v  2965  rr19.28v  2966  reu3  3016  uniiunlem  3338  reupick2  3519  rabxmdc  3554  uniss2  3966  ss2iun  4027  iineq2  4029  iunss2  4057  disjss2  4109  disjeq2  4110  disjnim  4120  repizf  4249  abnexg  4594  reusv3i  4607  tfis  4732  ssrel2  4867  issref  5173  dmmptg  5288  funco  5420  fununi  5452  fun11uni  5454  funimaexglem  5467  fnmpt  5513  fun11iun  5663  mpteqb  5799  chfnrn  5823  dffo5  5860  ffvresb  5874  fmptcof  5878  dfmptg  5891  mpo2eqb  6201  ralrnmpo  6206  rexrnmpo  6207  uchoice  6375  fnmpo  6442  mpoexxg  6450  smores  6567  riinerm  6886  ixpm  7016  difinfinf  7447  nninfwlpoimlemginf  7522  exmidontriimlem1  7583  onntri13  7603  onntri24  7607  cc4f  7641  cc4n  7643  cauappcvgprlemdisj  8024  caucvgsrlemasr  8163  caucvgsr  8175  suplocsr  8182  rexuz3  11778  recvguniq  11783  cau3lem  11903  caubnd2  11906  rexanre  12009  climi2  12079  climi0  12080  climcaucn  12142  ndvdssub  12722  gcdsupex  12759  gcdsupcl  12760  bezoutlemmo  12808  ptex  13677  mgmidmo  13751  issubg2m  14051  eltg2b  15280  neipsm  15380  lmcvg  15443  txlm  15505  metrest  15732  mulcncflem  15833  wlkvtxeledgg  16790  upgrwlkcompim  16808  upgrwlkvtxedg  16810  upgr2wlkdc  16823  bj-charfunbi  17042  bj-indint  17162  bj-indind  17163  bj-bdfindis  17178  setindis  17198  bdsetindis  17200  pw1dceq  17240  exmidcon  17242  exmidpeirce  17243  neap0mkv  17326