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 )

Syntax hints:   -> wi 4   e. wcel 2209   A.wral 2528

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 1500  ax-gen 1502

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

This theorem is referenced 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  3961  ss2iun  4022  iineq2  4024  iunss2  4052  disjss2  4104  disjeq2  4105  disjnim  4115  repizf  4242  abnexg  4587  reusv3i  4600  tfis  4725  ssrel2  4860  issref  5165  dmmptg  5280  funco  5412  fununi  5444  fun11uni  5446  funimaexglem  5459  fnmpt  5505  fun11iun  5655  mpteqb  5790  chfnrn  5811  dffo5  5848  ffvresb  5862  fmptcof  5866  dfmptg  5879  mpo2eqb  6188  ralrnmpo  6193  rexrnmpo  6194  uchoice  6361  fnmpo  6428  mpoexxg  6436  smores  6553  riinerm  6872  ixpm  7002  difinfinf  7431  nninfwlpoimlemginf  7506  exmidontriimlem1  7567  onntri13  7587  onntri24  7591  cc4f  7625  cc4n  7627  cauappcvgprlemdisj  8008  caucvgsrlemasr  8147  caucvgsr  8159  suplocsr  8166  rexuz3  11734  recvguniq  11739  cau3lem  11858  caubnd2  11861  rexanre  11964  climi2  12032  climi0  12033  climcaucn  12095  ndvdssub  12675  gcdsupex  12712  gcdsupcl  12713  bezoutlemmo  12761  ptex  13595  mgmidmo  13669  issubg2m  13969  eltg2b  15078  neipsm  15178  lmcvg  15241  txlm  15303  metrest  15530  mulcncflem  15631  wlkvtxeledgg  16499  upgrwlkcompim  16517  upgrwlkvtxedg  16519  upgr2wlkdc  16532  bj-charfunbi  16751  bj-indint  16871  bj-indind  16872  bj-bdfindis  16887  setindis  16907  bdsetindis  16909  pw1dceq  16948  exmidcon  16950  exmidpeirce  16951  neap0mkv  17024