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	$$⊢Ⅎx\phi$$
	dvelimdc.2	$$⊢Ⅎz\phi$$
	dvelimdc.3	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
	dvelimdc.4	$$⊢\phi \to \underset{\_}{Ⅎ}zB$$
	dvelimdc.5	$$⊢\phi \to \left(z=y\to A=B\right)$$
Assertion	dvelimdc	$$⊢\phi \to \left(\neg \forall xx=y\to \underset{\_}{Ⅎ}xB\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvelimdc.1	$$⊢Ⅎx\phi$$
2		dvelimdc.2	$$⊢Ⅎz\phi$$
3		dvelimdc.3	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
4		dvelimdc.4	$$⊢\phi \to \underset{\_}{Ⅎ}zB$$
5		dvelimdc.5	$$⊢\phi \to \left(z=y\to A=B\right)$$
6		nfv	$$⊢Ⅎw\left(\phi \wedge \neg \forall xx=y\right)$$
7	3	nfcrd	$$⊢\phi \to Ⅎxw\in A$$
8	4	nfcrd	$$⊢\phi \to Ⅎzw\in B$$
9		eleq2	$$⊢A=B\to \left(w\in A\leftrightarrow w\in B\right)$$
10	5 9	syl6	$$⊢\phi \to \left(z=y\to \left(w\in A\leftrightarrow w\in B\right)\right)$$
11	1 2 7 8 10	dvelimdf	$$⊢\phi \to \left(\neg \forall xx=y\to Ⅎxw\in B\right)$$
12	11	imp	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to Ⅎxw\in B$$
13	6 12	nfcd	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to \underset{\_}{Ⅎ}xB$$
14	13	ex	$$⊢\phi \to \left(\neg \forall xx=y\to \underset{\_}{Ⅎ}xB\right)$$