Theorem wl-mo2tf

Description: Closed form of mof with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 20-Sep-2020)

	Ref	Expression
Assertion	wl-mo2tf	$$⊢\left(\neg \forall xx=y\wedge \forall xℲy\phi \right)\to \left({\exists }^{*}x\phi \leftrightarrow \exists y\forall x\left(\phi \to x=y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfnae	$$⊢Ⅎx\neg \forall xx=y$$
2		nfa1	$$⊢Ⅎx\forall xℲy\phi$$
3	1 2	nfan	$$⊢Ⅎx\left(\neg \forall xx=y\wedge \forall xℲy\phi \right)$$
4		nfnae	$$⊢Ⅎy\neg \forall xx=y$$
5		nfnf1	$$⊢ℲyℲy\phi$$
6	5	nfal	$$⊢Ⅎy\forall xℲy\phi$$
7	4 6	nfan	$$⊢Ⅎy\left(\neg \forall xx=y\wedge \forall xℲy\phi \right)$$
8		simpl	$$⊢\left(\neg \forall xx=y\wedge \forall xℲy\phi \right)\to \neg \forall xx=y$$
9		sp	$$⊢\forall xℲy\phi \to Ⅎy\phi$$
10	9	adantl	$$⊢\left(\neg \forall xx=y\wedge \forall xℲy\phi \right)\to Ⅎy\phi$$
11	3 7 8 10	wl-mo2df	$$⊢\left(\neg \forall xx=y\wedge \forall xℲy\phi \right)\to \left({\exists }^{*}x\phi \leftrightarrow \exists y\forall x\left(\phi \to x=y\right)\right)$$