Theorem ralimi 2689

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 10	. 2 |- (x e. A -> (ph -> ps))
3	2	ralimia 2687	1 |- (A.x e. A ph -> A.x e. A ps)

Syntax hints:   -> wi 4   e. wcel 1710  A.wral 2614

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557

This theorem depends on definitions:  df-bi 177  df-ral 2619

This theorem is referenced by:  ral2imi  2690  r19.26  2746  r19.29  2754  rr19.3v  2980  rr19.28v  2981  reu3  3026  uniiunlem  3353  reupick2  3541  uniss2  3922  ss2iun  3984  iineq2  3986  iunss2  4011  fununi  5160  fun11uni  5162  dff3  5420  dffo5  5424  ffvresb  5431  dmmptg  5684  fnmpt  5689  fnmpt2  5732