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  4247  abnexg  4592  reusv3i  4605  tfis  4730  ssrel2  4865  issref  5170  dmmptg  5285  funco  5417  fununi  5449  fun11uni  5451  funimaexglem  5464  fnmpt  5510  fun11iun  5660  mpteqb  5796  chfnrn  5820  dffo5  5857  ffvresb  5871  fmptcof  5875  dfmptg  5888  mpo2eqb  6198  ralrnmpo  6203  rexrnmpo  6204  uchoice  6371  fnmpo  6438  mpoexxg  6446  smores  6563  riinerm  6882  ixpm  7012  difinfinf  7441  nninfwlpoimlemginf  7516  exmidontriimlem1  7577  onntri13  7597  onntri24  7601  cc4f  7635  cc4n  7637  cauappcvgprlemdisj  8018  caucvgsrlemasr  8157  caucvgsr  8169  suplocsr  8176  rexuz3  11756  recvguniq  11761  cau3lem  11880  caubnd2  11883  rexanre  11986  climi2  12054  climi0  12055  climcaucn  12117  ndvdssub  12697  gcdsupex  12734  gcdsupcl  12735  bezoutlemmo  12783  ptex  13618  mgmidmo  13692  issubg2m  13992  eltg2b  15155  neipsm  15255  lmcvg  15318  txlm  15380  metrest  15607  mulcncflem  15708  wlkvtxeledgg  16585  upgrwlkcompim  16603  upgrwlkvtxedg  16605  upgr2wlkdc  16618  bj-charfunbi  16837  bj-indint  16957  bj-indind  16958  bj-bdfindis  16973  setindis  16993  bdsetindis  16995  pw1dceq  17035  exmidcon  17037  exmidpeirce  17038  neap0mkv  17119