Theorem ralimi 2384

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

Syntax hints:   -> wi 4   e. wcel 1393   A.wral 2306

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338

This theorem depends on definitions:  df-bi 110  df-ral 2311

This theorem is referenced by:  ral2imi  2385  r19.26  2441  r19.29  2450  rr19.3v  2682  rr19.28v  2683  reu3  2731  uniiunlem  3028  reupick2  3223  uniss2  3611  ss2iun  3672  iineq2  3674  iunss2  3702  disjss2  3748  disjeq2  3749  repizf  3873  reusv3i  4191  tfis  4306  ssrel2  4430  issref  4707  dmmptg  4818  funco  4940  fununi  4967  fun11uni  4969  funimaexglem  4982  fnmpt  5025  fun11iun  5147  mpteqb  5261  chfnrn  5278  dffo5  5316  ffvresb  5328  fmptcof  5331  dfmptg  5342  mpt22eqb  5610  ralrnmpt2  5615  rexrnmpt2  5616  fnmpt2  5828  mpt2exxg  5833  smores  5907  riinerm  6179  cauappcvgprlemdisj  6749  caucvgsrlemasr  6874  caucvgsr  6886  rexuz3  9588  recvguniq  9593  cau3lem  9710  caubnd2  9713  climi2  9809  climi0  9810  climcaucn  9870  bj-indint  10055  bj-indind  10056  bj-bdfindis  10072  setindis  10092  bdsetindis  10094