Theorem wl-mo2t

Description: Closed form of mof . (Contributed by Wolf Lammen, 18-Aug-2019)

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

Proof

Step	Hyp	Ref	Expression
1		dfmo	$$⊢{\exists }^{*}x\phi \leftrightarrow \exists u\forall x\left(\phi \to x=u\right)$$
2		nfnf1	$$⊢ℲyℲy\phi$$
3	2	nfal	$$⊢Ⅎy\forall xℲy\phi$$
4		nfa1	$$⊢Ⅎx\forall xℲy\phi$$
5		sp	$$⊢\forall xℲy\phi \to Ⅎy\phi$$
6		nfvd	$$⊢\forall xℲy\phi \to Ⅎyx=u$$
7	5 6	nfimd	$$⊢\forall xℲy\phi \to Ⅎy\left(\phi \to x=u\right)$$
8	4 7	nfald	$$⊢\forall xℲy\phi \to Ⅎy\forall x\left(\phi \to x=u\right)$$
9		equequ2	$$⊢u=y\to \left(x=u\leftrightarrow x=y\right)$$
10	9	imbi2d	$$⊢u=y\to \left(\left(\phi \to x=u\right)\leftrightarrow \left(\phi \to x=y\right)\right)$$
11	10	albidv	$$⊢u=y\to \left(\forall x\left(\phi \to x=u\right)\leftrightarrow \forall x\left(\phi \to x=y\right)\right)$$
12	11	a1i	$$⊢\forall xℲy\phi \to \left(u=y\to \left(\forall x\left(\phi \to x=u\right)\leftrightarrow \forall x\left(\phi \to x=y\right)\right)\right)$$
13	3 8 12	cbvexdw	$$⊢\forall xℲy\phi \to \left(\exists u\forall x\left(\phi \to x=u\right)\leftrightarrow \exists y\forall x\left(\phi \to x=y\right)\right)$$
14	1 13	bitrid	$$⊢\forall xℲy\phi \to \left({\exists }^{*}x\phi \leftrightarrow \exists y\forall x\left(\phi \to x=y\right)\right)$$