Theorem dvelimf

Description: Version of dvelimv without any variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 1-Oct-2002) (Revised by Mario Carneiro, 6-Oct-2016) (Proof shortened by Wolf Lammen, 11-May-2018) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dvelimf.1	$$⊢Ⅎx\phi$$
	dvelimf.2	$$⊢Ⅎz\psi$$
	dvelimf.3	$$⊢z=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	dvelimf	$$⊢\neg \forall xx=y\to Ⅎx\psi$$

Proof

Step	Hyp	Ref	Expression
1		dvelimf.1	$$⊢Ⅎx\phi$$
2		dvelimf.2	$$⊢Ⅎz\psi$$
3		dvelimf.3	$$⊢z=y\to \left(\phi \leftrightarrow \psi \right)$$
4	2 3	equsal	$$⊢\forall z\left(z=y\to \phi \right)\leftrightarrow \psi$$
5	4	bicomi	$$⊢\psi \leftrightarrow \forall z\left(z=y\to \phi \right)$$
6		nfnae	$$⊢Ⅎz\neg \forall xx=y$$
7		nfeqf	$$⊢\left(\neg \forall xx=z\wedge \neg \forall xx=y\right)\to Ⅎxz=y$$
8	7	ancoms	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎxz=y$$
9	1	a1i	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎx\phi$$
10	8 9	nfimd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎx\left(z=y\to \phi \right)$$
11	6 10	nfald2	$$⊢\neg \forall xx=y\to Ⅎx\forall z\left(z=y\to \phi \right)$$
12	5 11	nfxfrd	$$⊢\neg \forall xx=y\to Ⅎx\psi$$