Metamath Proof Explorer


Theorem speimfw

Description: Specialization, with additional weakening (compared to 19.2 ) 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, 5-Dec-2017)

Ref Expression
Hypothesis speimfw.2
|- ( x = y -> ( ph -> ps ) )
Assertion speimfw
|- ( -. A. x -. x = y -> ( A. x ph -> E. x ps ) )

Proof

Step Hyp Ref Expression
1 speimfw.2
 |-  ( x = y -> ( ph -> ps ) )
2 df-ex
 |-  ( E. x x = y <-> -. A. x -. x = y )
3 2 biimpri
 |-  ( -. A. x -. x = y -> E. x x = y )
4 1 com12
 |-  ( ph -> ( x = y -> ps ) )
5 4 aleximi
 |-  ( A. x ph -> ( E. x x = y -> E. x ps ) )
6 3 5 syl5com
 |-  ( -. A. x -. x = y -> ( A. x ph -> E. x ps ) )