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		equequ2	$$⊢y=z\to \left(x=y\leftrightarrow x=z\right)$$
6	5	imbi2d	$$⊢y=z\to \left(\left(\phi \to x=y\right)\leftrightarrow \left(\phi \to x=z\right)\right)$$
7	6	albidv	$$⊢y=z\to \left(\forall x\left(\phi \to x=y\right)\leftrightarrow \forall x\left(\phi \to x=z\right)\right)$$
8	7	19.8aw	$$⊢\forall x\left(\phi \to x=y\right)\to \exists y\forall x\left(\phi \to x=y\right)$$
9		dfmo	$$⊢{\exists }^{*}x\phi \leftrightarrow \exists y\forall x\left(\phi \to x=y\right)$$
10	8 9	sylibr	$$⊢\forall x\left(\phi \to x=y\right)\to {\exists }^{*}x\phi$$
11	4 10	vtoclg	$$⊢A\in \mathrm{V}\to \left(\forall x\left(\phi \to x=A\right)\to {\exists }^{*}x\phi \right)$$
12		eqvisset	$$⊢x=A\to A\in \mathrm{V}$$
13	12	imim2i	$$⊢\left(\phi \to x=A\right)\to \left(\phi \to A\in \mathrm{V}\right)$$
14	13	con3rr3	$$⊢\neg A\in \mathrm{V}\to \left(\left(\phi \to x=A\right)\to \neg \phi \right)$$
15	14	alimdv	$$⊢\neg A\in \mathrm{V}\to \left(\forall x\left(\phi \to x=A\right)\to \forall x\neg \phi \right)$$
16		alnex	$$⊢\forall x\neg \phi \leftrightarrow \neg \exists x\phi$$
17		nexmo	$$⊢\neg \exists x\phi \to {\exists }^{*}x\phi$$
18	16 17	sylbi	$$⊢\forall x\neg \phi \to {\exists }^{*}x\phi$$
19	15 18	syl6	$$⊢\neg A\in \mathrm{V}\to \left(\forall x\left(\phi \to x=A\right)\to {\exists }^{*}x\phi \right)$$
20	11 19	pm2.61i	$$⊢\forall x\left(\phi \to x=A\right)\to {\exists }^{*}x\phi$$