Theorem ralimi 2553

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

Syntax hints:   -> wi 4   e. wcel 2160   A.wral 2468

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 2473

This theorem is referenced by:  2ralimi  2554  ral2imi  2555  r19.26  2616  r19.29  2627  rr19.3v  2891  rr19.28v  2892  reu3  2942  uniiunlem  3259  reupick2  3436  uniss2  3855  ss2iun  3916  iineq2  3918  iunss2  3946  disjss2  3998  disjeq2  3999  disjnim  4009  repizf  4134  abnexg  4464  reusv3i  4477  tfis  4600  ssrel2  4734  issref  5029  dmmptg  5144  funco  5275  fununi  5303  fun11uni  5305  funimaexglem  5318  fnmpt  5361  fun11iun  5501  mpteqb  5626  chfnrn  5647  dffo5  5685  ffvresb  5699  fmptcof  5703  dfmptg  5715  mpo2eqb  6005  ralrnmpo  6010  rexrnmpo  6011  fnmpo  6226  mpoexxg  6234  smores  6316  riinerm  6633  ixpm  6755  difinfinf  7129  nninfwlpoimlemginf  7203  exmidontriimlem1  7249  onntri13  7266  onntri24  7270  cc4f  7297  cc4n  7299  cauappcvgprlemdisj  7679  caucvgsrlemasr  7818  caucvgsr  7830  suplocsr  7837  rexuz3  11030  recvguniq  11035  cau3lem  11154  caubnd2  11157  rexanre  11260  climi2  11327  climi0  11328  climcaucn  11390  ndvdssub  11966  gcdsupex  11989  gcdsupcl  11990  bezoutlemmo  12038  ptex  12766  mgmidmo  12845  issubg2m  13125  eltg2b  14006  neipsm  14106  lmcvg  14169  txlm  14231  metrest  14458  mulcncflem  14542  bj-charfunbi  15016  bj-indint  15136  bj-indind  15137  bj-bdfindis  15152  setindis  15172  bdsetindis  15174  neap0mkv  15271