Theorem ralimi 2557

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

Syntax hints:   -> wi 4   e. wcel 2164   A.wral 2472

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 1458  ax-gen 1460

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

This theorem is referenced by:  2ralimi  2558  ral2imi  2559  r19.26  2620  r19.29  2631  rr19.3v  2900  rr19.28v  2901  reu3  2951  uniiunlem  3269  reupick2  3446  uniss2  3867  ss2iun  3928  iineq2  3930  iunss2  3958  disjss2  4010  disjeq2  4011  disjnim  4021  repizf  4146  abnexg  4478  reusv3i  4491  tfis  4616  ssrel2  4750  issref  5049  dmmptg  5164  funco  5295  fununi  5323  fun11uni  5325  funimaexglem  5338  fnmpt  5381  fun11iun  5522  mpteqb  5649  chfnrn  5670  dffo5  5708  ffvresb  5722  fmptcof  5726  dfmptg  5738  mpo2eqb  6029  ralrnmpo  6034  rexrnmpo  6035  uchoice  6192  fnmpo  6257  mpoexxg  6265  smores  6347  riinerm  6664  ixpm  6786  difinfinf  7162  nninfwlpoimlemginf  7237  exmidontriimlem1  7283  onntri13  7300  onntri24  7304  cc4f  7331  cc4n  7333  cauappcvgprlemdisj  7713  caucvgsrlemasr  7852  caucvgsr  7864  suplocsr  7871  rexuz3  11137  recvguniq  11142  cau3lem  11261  caubnd2  11264  rexanre  11367  climi2  11434  climi0  11435  climcaucn  11497  ndvdssub  12074  gcdsupex  12097  gcdsupcl  12098  bezoutlemmo  12146  ptex  12878  mgmidmo  12958  issubg2m  13262  eltg2b  14233  neipsm  14333  lmcvg  14396  txlm  14458  metrest  14685  mulcncflem  14786  bj-charfunbi  15373  bj-indint  15493  bj-indind  15494  bj-bdfindis  15509  setindis  15529  bdsetindis  15531  neap0mkv  15629