Theorem dvelimdc

Description: Deduction form of dvelimc . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Mario Carneiro, 8-Oct-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dvelimdc.1	|- F/ x ph
	dvelimdc.2	|- F/ z ph
	dvelimdc.3	|- ( ph -> F/_ x A )
	dvelimdc.4	|- ( ph -> F/_ z B )
	dvelimdc.5	|- ( ph -> ( z = y -> A = B ) )
Assertion	dvelimdc	|- ( ph -> ( -. A. x x = y -> F/_ x B ) )

Proof

Step	Hyp	Ref	Expression
1		dvelimdc.1	|- F/ x ph
2		dvelimdc.2	|- F/ z ph
3		dvelimdc.3	|- ( ph -> F/_ x A )
4		dvelimdc.4	|- ( ph -> F/_ z B )
5		dvelimdc.5	|- ( ph -> ( z = y -> A = B ) )
6		nfv	|- F/ w ( ph /\ -. A. x x = y )
7	3	nfcrd	|- ( ph -> F/ x w e. A )
8	4	nfcrd	|- ( ph -> F/ z w e. B )
9		eleq2	|- ( A = B -> ( w e. A <-> w e. B ) )
10	5 9	syl6	|- ( ph -> ( z = y -> ( w e. A <-> w e. B ) ) )
11	1 2 7 8 10	dvelimdf	|- ( ph -> ( -. A. x x = y -> F/ x w e. B ) )
12	11	imp	|- ( ( ph /\ -. A. x x = y ) -> F/ x w e. B )
13	6 12	nfcd	|- ( ( ph /\ -. A. x x = y ) -> F/_ x B )
14	13	ex	|- ( ph -> ( -. A. x x = y -> F/_ x B ) )