Theorem bj-dvelimdv1

Description: Curried (exported) form of bj-dvelimdv (of course, one is directly provable from the other, but we keep this proof for illustration purposes). (Contributed by BJ, 20-Oct-2021) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	bj-dvelimdv.nf	$$⊢\phi \to Ⅎx\chi$$
	bj-dvelimdv.is	$$⊢z=y\to \left(\chi \leftrightarrow \psi \right)$$
Assertion	bj-dvelimdv1	$$⊢\phi \to \left(\neg \forall xx=y\to Ⅎx\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-dvelimdv.nf	$$⊢\phi \to Ⅎx\chi$$
2		bj-dvelimdv.is	$$⊢z=y\to \left(\chi \leftrightarrow \psi \right)$$
3		nfeqf2	$$⊢\neg \forall xx=y\to Ⅎxz=y$$
4		bj-nfimt	$$⊢Ⅎxz=y\to \left(Ⅎx\chi \to Ⅎx\left(z=y\to \chi \right)\right)$$
5	3 1 4	syl2imc	$$⊢\phi \to \left(\neg \forall xx=y\to Ⅎx\left(z=y\to \chi \right)\right)$$
6	5	alrimdv	$$⊢\phi \to \left(\neg \forall xx=y\to \forall zℲx\left(z=y\to \chi \right)\right)$$
7		bj-nfalt	$$⊢\forall zℲx\left(z=y\to \chi \right)\to Ⅎx\forall z\left(z=y\to \chi \right)$$
8	2	equsalvw	$$⊢\forall z\left(z=y\to \chi \right)\leftrightarrow \psi$$
9	8	nfbii	$$⊢Ⅎx\forall z\left(z=y\to \chi \right)\leftrightarrow Ⅎx\psi$$
10	6 7 9	bj-syl66ib	$$⊢\phi \to \left(\neg \forall xx=y\to Ⅎx\psi \right)$$