Theorem dvelimdf

Description: Deduction form of dvelimf . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 7-Apr-2004) (Revised by Mario Carneiro, 6-Oct-2016) (Proof shortened by Wolf Lammen, 11-May-2018) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dvelimdf.1	|- F/ x ph
	dvelimdf.2	|- F/ z ph
	dvelimdf.3	|- ( ph -> F/ x ps )
	dvelimdf.4	|- ( ph -> F/ z ch )
	dvelimdf.5	|- ( ph -> ( z = y -> ( ps <-> ch ) ) )
Assertion	dvelimdf	|- ( ph -> ( -. A. x x = y -> F/ x ch ) )

Proof

Step	Hyp	Ref	Expression
1		dvelimdf.1	|- F/ x ph
2		dvelimdf.2	|- F/ z ph
3		dvelimdf.3	|- ( ph -> F/ x ps )
4		dvelimdf.4	|- ( ph -> F/ z ch )
5		dvelimdf.5	|- ( ph -> ( z = y -> ( ps <-> ch ) ) )
6	1 3	nfim1	|- F/ x ( ph -> ps )
7	2 4	nfim1	|- F/ z ( ph -> ch )
8	5	com12	|- ( z = y -> ( ph -> ( ps <-> ch ) ) )
9	8	pm5.74d	|- ( z = y -> ( ( ph -> ps ) <-> ( ph -> ch ) ) )
10	6 7 9	dvelimf	|- ( -. A. x x = y -> F/ x ( ph -> ch ) )
11		pm5.5	|- ( ph -> ( ( ph -> ch ) <-> ch ) )
12	1 11	nfbidf	|- ( ph -> ( F/ x ( ph -> ch ) <-> F/ x ch ) )
13	10 12	imbitrid	|- ( ph -> ( -. A. x x = y -> F/ x ch ) )