Theorem ralimi 2690

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

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

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

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

This theorem is referenced by:  ral2imi  2691  r19.26  2747  r19.29  2755  rr19.3v  2981  rr19.28v  2982  reu3  3027  uniiunlem  3354  reupick2  3542  uniss2  3923  ss2iun  3985  iineq2  3987  iunss2  4012  fununi  5161  fun11uni  5163  dff3  5421  dffo5  5425  ffvresb  5432  dmmptg  5685  fnmpt  5690  fnmpt2  5733