Theorem ralimi 2569

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

Syntax hints:   -> wi 4   e. wcel 2176   A.wral 2484

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 1470  ax-gen 1472

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

This theorem is referenced by:  2ralimi  2570  ral2imi  2571  r19.26  2632  r19.29  2643  rr19.3v  2912  rr19.28v  2913  reu3  2963  uniiunlem  3282  reupick2  3459  uniss2  3881  ss2iun  3942  iineq2  3944  iunss2  3972  disjss2  4024  disjeq2  4025  disjnim  4035  repizf  4160  abnexg  4493  reusv3i  4506  tfis  4631  ssrel2  4765  issref  5065  dmmptg  5180  funco  5311  fununi  5342  fun11uni  5344  funimaexglem  5357  fnmpt  5402  fun11iun  5543  mpteqb  5670  chfnrn  5691  dffo5  5729  ffvresb  5743  fmptcof  5747  dfmptg  5759  mpo2eqb  6055  ralrnmpo  6060  rexrnmpo  6061  uchoice  6223  fnmpo  6288  mpoexxg  6296  smores  6378  riinerm  6695  ixpm  6817  difinfinf  7203  nninfwlpoimlemginf  7278  exmidontriimlem1  7333  onntri13  7350  onntri24  7354  cc4f  7381  cc4n  7383  cauappcvgprlemdisj  7764  caucvgsrlemasr  7903  caucvgsr  7915  suplocsr  7922  rexuz3  11301  recvguniq  11306  cau3lem  11425  caubnd2  11428  rexanre  11531  climi2  11599  climi0  11600  climcaucn  11662  ndvdssub  12241  gcdsupex  12278  gcdsupcl  12279  bezoutlemmo  12327  ptex  13096  mgmidmo  13204  issubg2m  13525  eltg2b  14526  neipsm  14626  lmcvg  14689  txlm  14751  metrest  14978  mulcncflem  15079  bj-charfunbi  15747  bj-indint  15867  bj-indind  15868  bj-bdfindis  15883  setindis  15903  bdsetindis  15905  neap0mkv  16008