Theorem ralimi 2560

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

Syntax hints:   -> wi 4   e. wcel 2167   A.wral 2475

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 1461  ax-gen 1463

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

This theorem is referenced by:  2ralimi  2561  ral2imi  2562  r19.26  2623  r19.29  2634  rr19.3v  2903  rr19.28v  2904  reu3  2954  uniiunlem  3272  reupick2  3449  uniss2  3870  ss2iun  3931  iineq2  3933  iunss2  3961  disjss2  4013  disjeq2  4014  disjnim  4024  repizf  4149  abnexg  4481  reusv3i  4494  tfis  4619  ssrel2  4753  issref  5052  dmmptg  5167  funco  5298  fununi  5326  fun11uni  5328  funimaexglem  5341  fnmpt  5384  fun11iun  5525  mpteqb  5652  chfnrn  5673  dffo5  5711  ffvresb  5725  fmptcof  5729  dfmptg  5741  mpo2eqb  6032  ralrnmpo  6037  rexrnmpo  6038  uchoice  6195  fnmpo  6260  mpoexxg  6268  smores  6350  riinerm  6667  ixpm  6789  difinfinf  7167  nninfwlpoimlemginf  7242  exmidontriimlem1  7288  onntri13  7305  onntri24  7309  cc4f  7336  cc4n  7338  cauappcvgprlemdisj  7718  caucvgsrlemasr  7857  caucvgsr  7869  suplocsr  7876  rexuz3  11155  recvguniq  11160  cau3lem  11279  caubnd2  11282  rexanre  11385  climi2  11453  climi0  11454  climcaucn  11516  ndvdssub  12095  gcdsupex  12124  gcdsupcl  12125  bezoutlemmo  12173  ptex  12935  mgmidmo  13015  issubg2m  13319  eltg2b  14290  neipsm  14390  lmcvg  14453  txlm  14515  metrest  14742  mulcncflem  14843  bj-charfunbi  15457  bj-indint  15577  bj-indind  15578  bj-bdfindis  15593  setindis  15613  bdsetindis  15615  neap0mkv  15713