Theorem wl-sb8mot

Description: Substitution of variable in universal quantifier. Closed form of sb8mo . (Contributed by Wolf Lammen, 11-Aug-2019)

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

Proof

Step	Hyp	Ref	Expression
1		wl-sb8et	$$⊢\forall xℲy\phi \to \left(\exists x\phi \leftrightarrow \exists y\left[y/x\right]\phi \right)$$
2		wl-sb8eut	$$⊢\forall xℲy\phi \to \left(\exists !x\phi \leftrightarrow \exists !y\left[y/x\right]\phi \right)$$
3	1 2	imbi12d	$$⊢\forall xℲy\phi \to \left(\left(\exists x\phi \to \exists !x\phi \right)\leftrightarrow \left(\exists y\left[y/x\right]\phi \to \exists !y\left[y/x\right]\phi \right)\right)$$
4		moeu	$$⊢{\exists }^{*}x\phi \leftrightarrow \left(\exists x\phi \to \exists !x\phi \right)$$
5		moeu	$$⊢{\exists }^{*}y\left[y/x\right]\phi \leftrightarrow \left(\exists y\left[y/x\right]\phi \to \exists !y\left[y/x\right]\phi \right)$$
6	3 4 5	3bitr4g	$$⊢\forall xℲy\phi \to \left({\exists }^{*}x\phi \leftrightarrow {\exists }^{*}y\left[y/x\right]\phi \right)$$