Theorem wl-eudf

Description: Version of eu6 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, 23-Sep-2020)

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

Proof

Step	Hyp	Ref	Expression
1		wl-eudf.1	$$⊢Ⅎx\phi$$
2		wl-eudf.2	$$⊢Ⅎy\phi$$
3		wl-eudf.3	$$⊢\phi \to \neg \forall xx=y$$
4		wl-eudf.4	$$⊢\phi \to Ⅎy\psi$$
5		eu6	$$⊢\exists !x\psi \leftrightarrow \exists u\forall x\left(\psi \leftrightarrow 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	nfbid	$$⊢\phi \to Ⅎy\left(\psi \leftrightarrow x=u\right)$$
10	1 9	nfald	$$⊢\phi \to Ⅎy\forall x\left(\psi \leftrightarrow 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	bibi2d	$$⊢u=y\to \left(\left(\psi \leftrightarrow x=u\right)\leftrightarrow \left(\psi \leftrightarrow x=y\right)\right)$$
16	15	adantl	$$⊢\left(\neg \forall xx=y\wedge u=y\right)\to \left(\left(\psi \leftrightarrow x=u\right)\leftrightarrow \left(\psi \leftrightarrow x=y\right)\right)$$
17	13 16	albid	$$⊢\left(\neg \forall xx=y\wedge u=y\right)\to \left(\forall x\left(\psi \leftrightarrow x=u\right)\leftrightarrow \forall x\left(\psi \leftrightarrow x=y\right)\right)$$
18	3 17	sylan	$$⊢\left(\phi \wedge u=y\right)\to \left(\forall x\left(\psi \leftrightarrow x=u\right)\leftrightarrow \forall x\left(\psi \leftrightarrow x=y\right)\right)$$
19	18	ex	$$⊢\phi \to \left(u=y\to \left(\forall x\left(\psi \leftrightarrow x=u\right)\leftrightarrow \forall x\left(\psi \leftrightarrow x=y\right)\right)\right)$$
20	2 10 19	cbvexd	$$⊢\phi \to \left(\exists u\forall x\left(\psi \leftrightarrow x=u\right)\leftrightarrow \exists y\forall x\left(\psi \leftrightarrow x=y\right)\right)$$
21	5 20	bitrid	$$⊢\phi \to \left(\exists !x\psi \leftrightarrow \exists y\forall x\left(\psi \leftrightarrow x=y\right)\right)$$