Theorem dvelimhw

Description: Proof of dvelimh without using ax-13 but with additional distinct variable conditions. (Contributed by NM, 1-Oct-2002) (Revised by Andrew Salmon, 21-Jul-2011) (Revised by NM, 1-Aug-2017) (Proof shortened by Wolf Lammen, 23-Dec-2018)

	Ref	Expression
Hypotheses	dvelimhw.1	|- ( ph -> A. x ph )
	dvelimhw.2	|- ( ps -> A. z ps )
	dvelimhw.3	|- ( z = y -> ( ph <-> ps ) )
	dvelimhw.4	|- ( -. A. x x = y -> ( y = z -> A. x y = z ) )
Assertion	dvelimhw	|- ( -. A. x x = y -> ( ps -> A. x ps ) )

Proof

Step	Hyp	Ref	Expression
1		dvelimhw.1	|- ( ph -> A. x ph )
2		dvelimhw.2	|- ( ps -> A. z ps )
3		dvelimhw.3	|- ( z = y -> ( ph <-> ps ) )
4		dvelimhw.4	|- ( -. A. x x = y -> ( y = z -> A. x y = z ) )
5		nfv	|- F/ z -. A. x x = y
6		equcom	|- ( z = y <-> y = z )
7		nfna1	|- F/ x -. A. x x = y
8	7 4	nf5d	|- ( -. A. x x = y -> F/ x y = z )
9	6 8	nfxfrd	|- ( -. A. x x = y -> F/ x z = y )
10	1	nf5i	|- F/ x ph
11	10	a1i	|- ( -. A. x x = y -> F/ x ph )
12	9 11	nfimd	|- ( -. A. x x = y -> F/ x ( z = y -> ph ) )
13	5 12	nfald	|- ( -. A. x x = y -> F/ x A. z ( z = y -> ph ) )
14	2 3	equsalhw	|- ( A. z ( z = y -> ph ) <-> ps )
15	14	nfbii	|- ( F/ x A. z ( z = y -> ph ) <-> F/ x ps )
16	13 15	sylib	|- ( -. A. x x = y -> F/ x ps )
17	16	nf5rd	|- ( -. A. x x = y -> ( ps -> A. x ps ) )