Theorem mo

Description: Equivalent definitions of "there exists at most one". (Contributed by NM, 7-Aug-1994) (Revised by Mario Carneiro, 7-Oct-2016) (Proof shortened by Wolf Lammen, 2-Dec-2018)

	Ref	Expression
Hypothesis	mo.nf	$$⊢Ⅎy\phi$$
Assertion	mo	$$⊢\exists y\forall x\left(\phi \to x=y\right)\leftrightarrow \forall x\forall y\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)$$

Proof

Step	Hyp	Ref	Expression
1		mo.nf	$$⊢Ⅎy\phi$$
2	1	mof	$$⊢{\exists }^{*}x\phi \leftrightarrow \exists y\forall x\left(\phi \to x=y\right)$$
3	1	mo3	$$⊢{\exists }^{*}x\phi \leftrightarrow \forall x\forall y\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)$$
4	2 3	bitr3i	$$⊢\exists y\forall x\left(\phi \to x=y\right)\leftrightarrow \forall x\forall y\left(\left(\phi \wedge \left[y/x\right]\phi \right)\to x=y\right)$$