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 ) )