Theorem mo2icl

Description: Theorem for inferring "at most one." (Contributed by NM, 17-Oct-1996)

	Ref	Expression
Assertion	mo2icl	$$⊢\forall x\left(\phi \to x=A\right)\to {\exists }^{*}x\phi$$

Proof

Step	Hyp	Ref	Expression
1		eqeq2	$$⊢y=A\to \left(x=y\leftrightarrow x=A\right)$$
2	1	imbi2d	$$⊢y=A\to \left(\left(\phi \to x=y\right)\leftrightarrow \left(\phi \to x=A\right)\right)$$
3	2	albidv	$$⊢y=A\to \left(\forall x\left(\phi \to x=y\right)\leftrightarrow \forall x\left(\phi \to x=A\right)\right)$$
4	3	imbi1d	$$⊢y=A\to \left(\left(\forall x\left(\phi \to x=y\right)\to {\exists }^{*}x\phi \right)\leftrightarrow \left(\forall x\left(\phi \to x=A\right)\to {\exists }^{*}x\phi \right)\right)$$
5		19.8a	$$⊢\forall x\left(\phi \to x=y\right)\to \exists y\forall x\left(\phi \to x=y\right)$$
6		df-mo	$$⊢{\exists }^{*}x\phi \leftrightarrow \exists y\forall x\left(\phi \to x=y\right)$$
7	5 6	sylibr	$$⊢\forall x\left(\phi \to x=y\right)\to {\exists }^{*}x\phi$$
8	4 7	vtoclg	$$⊢A\in \mathrm{V}\to \left(\forall x\left(\phi \to x=A\right)\to {\exists }^{*}x\phi \right)$$
9		eqvisset	$$⊢x=A\to A\in \mathrm{V}$$
10	9	imim2i	$$⊢\left(\phi \to x=A\right)\to \left(\phi \to A\in \mathrm{V}\right)$$
11	10	con3rr3	$$⊢\neg A\in \mathrm{V}\to \left(\left(\phi \to x=A\right)\to \neg \phi \right)$$
12	11	alimdv	$$⊢\neg A\in \mathrm{V}\to \left(\forall x\left(\phi \to x=A\right)\to \forall x\neg \phi \right)$$
13		alnex	$$⊢\forall x\neg \phi \leftrightarrow \neg \exists x\phi$$
14		nexmo	$$⊢\neg \exists x\phi \to {\exists }^{*}x\phi$$
15	13 14	sylbi	$$⊢\forall x\neg \phi \to {\exists }^{*}x\phi$$
16	12 15	syl6	$$⊢\neg A\in \mathrm{V}\to \left(\forall x\left(\phi \to x=A\right)\to {\exists }^{*}x\phi \right)$$
17	8 16	pm2.61i	$$⊢\forall x\left(\phi \to x=A\right)\to {\exists }^{*}x\phi$$