Theorem wl-mo2df

Description: Version of mof with a context and a distinctor replacing a distinct variable condition. This version should be used only to eliminate disjoint variable conditions. (Contributed by Wolf Lammen, 11-Aug-2019)

	Ref	Expression
Hypotheses	wl-mo2df.1	$$⊢Ⅎx\phi$$
	wl-mo2df.2	$$⊢Ⅎy\phi$$
	wl-mo2df.3	$$⊢\phi \to \neg \forall xx=y$$
	wl-mo2df.4	$$⊢\phi \to Ⅎy\psi$$
Assertion	wl-mo2df	$$⊢\phi \to \left({\exists }^{*}x\psi \leftrightarrow \exists y\forall x\left(\psi \to x=y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		wl-mo2df.1	$$⊢Ⅎx\phi$$
2		wl-mo2df.2	$$⊢Ⅎy\phi$$
3		wl-mo2df.3	$$⊢\phi \to \neg \forall xx=y$$
4		wl-mo2df.4	$$⊢\phi \to Ⅎy\psi$$
5		df-mo	$$⊢{\exists }^{*}x\psi \leftrightarrow \exists u\forall x\left(\psi \to x=u\right)$$
6		nfeqf1	$$⊢\neg \forall yy=x\to Ⅎyx=u$$
7	6	naecoms	$$⊢\neg \forall xx=y\to Ⅎyx=u$$
8	3 7	syl	$$⊢\phi \to Ⅎyx=u$$
9	4 8	nfimd	$$⊢\phi \to Ⅎy\left(\psi \to x=u\right)$$
10	1 9	nfald	$$⊢\phi \to Ⅎy\forall x\left(\psi \to x=u\right)$$
11		nfnae	$$⊢Ⅎx\neg \forall xx=y$$
12		nfeqf2	$$⊢\neg \forall xx=y\to Ⅎxu=y$$
13	11 12	nfan1	$$⊢Ⅎx\left(\neg \forall xx=y\wedge u=y\right)$$
14		equequ2	$$⊢u=y\to \left(x=u\leftrightarrow x=y\right)$$
15	14	imbi2d	$$⊢u=y\to \left(\left(\psi \to x=u\right)\leftrightarrow \left(\psi \to x=y\right)\right)$$
16	15	adantl	$$⊢\left(\neg \forall xx=y\wedge u=y\right)\to \left(\left(\psi \to x=u\right)\leftrightarrow \left(\psi \to x=y\right)\right)$$
17	13 16	albid	$$⊢\left(\neg \forall xx=y\wedge u=y\right)\to \left(\forall x\left(\psi \to x=u\right)\leftrightarrow \forall x\left(\psi \to x=y\right)\right)$$
18	3 17	sylan	$$⊢\left(\phi \wedge u=y\right)\to \left(\forall x\left(\psi \to x=u\right)\leftrightarrow \forall x\left(\psi \to x=y\right)\right)$$
19	18	ex	$$⊢\phi \to \left(u=y\to \left(\forall x\left(\psi \to x=u\right)\leftrightarrow \forall x\left(\psi \to x=y\right)\right)\right)$$
20	2 10 19	cbvexd	$$⊢\phi \to \left(\exists u\forall x\left(\psi \to x=u\right)\leftrightarrow \exists y\forall x\left(\psi \to x=y\right)\right)$$
21	5 20	bitrid	$$⊢\phi \to \left({\exists }^{*}x\psi \leftrightarrow \exists y\forall x\left(\psi \to x=y\right)\right)$$