Metamath Proof Explorer


Theorem spimfw

Description: Specialization, with additional weakening (compared to sp ) to allow bundling of x and y . Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-2017) (Proof shortened by Wolf Lammen, 7-Aug-2017)

Ref Expression
Hypotheses spimfw.1
|- ( -. ps -> A. x -. ps )
spimfw.2
|- ( x = y -> ( ph -> ps ) )
Assertion spimfw
|- ( -. A. x -. x = y -> ( A. x ph -> ps ) )

Proof

Step Hyp Ref Expression
1 spimfw.1
 |-  ( -. ps -> A. x -. ps )
2 spimfw.2
 |-  ( x = y -> ( ph -> ps ) )
3 2 speimfw
 |-  ( -. A. x -. x = y -> ( A. x ph -> E. x ps ) )
4 df-ex
 |-  ( E. x ps <-> -. A. x -. ps )
5 1 con1i
 |-  ( -. A. x -. ps -> ps )
6 4 5 sylbi
 |-  ( E. x ps -> ps )
7 3 6 syl6
 |-  ( -. A. x -. x = y -> ( A. x ph -> ps ) )