Theorem mo

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.)

Hypothesis
mo.nf
\( \vdash \Finv y \, \varphi \)
Conclusion
\( \vdash \exists y \, \forall x \, (\varphi \rightarrow x = y) \leftrightarrow \forall x \, \forall y \, (\varphi \wedge [ y / x ] \, \varphi \rightarrow x = y) \)
Proof
mo.nf
l1
mof _
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists y \, \forall x \, (\varphi \rightarrow x = y) \)
mo.nf
mo3 _
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \forall x \, \forall y \, (\varphi \wedge [ y / x ] \, \varphi \rightarrow x = y) \)
bitr3i l1 _