Theorem r19.20si 1254

Description: Inference quantifying both antecedent and consequent, with strong hypothesis.

Hypothesis

Ref	Expression
r19.20si.1	|- (ph -> ps)

Assertion

Ref	Expression
r19.20si	|- (A.x e. A ph -> A.x e. A ps)

Proof of Theorem r19.20si

Step	Hyp	Ref	Expression
1		r19.20si.1	. . 3 |- (ph -> ps)
2	1	a1i 7	. 2 |- (x e. A -> (ph -> ps))
3	2	r19.20i 1253	1 |- (A.x e. A ph -> A.x e. A ps)

Syntax hints:   -> wi 2   e. wcel 1092  A.wral 1201

This theorem is referenced by:  uniss2 1942  iunss2 2021  tfis 2245  find 2396  dffun7 2688  fununi 2705  fun11uni 2707  zfrep6 2744  fnopabg 2745  fopab2 2891  rankonid 3538  aceq5 3563  ac5b 3574  ac6lem 3575  ac6 3576  kmlem6 3585  kmlem12 3591  kmlem13 3592  projlem22 5214  stge0t 5673  stle1t 5674  mdbr3 5729  mdbr4 5730

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677

This theorem depends on definitions:  df-bi 128  df-ral 1205

metamath.org