Theorem nfmo1

Bound-variable hypothesis builder for the at-most-one quantifier. (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.) Adapt to new definition. (Revised by BJ, 1-Oct-2022.)

Conclusion
\( \vdash \Finv x \, \exists^\ast x \, \varphi \)
Proof
l0
dfmo
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists y \, \forall x \, (\varphi \rightarrow x = y) \)
nfexa2
\( \vdash \Finv x \, \exists y \, \forall x \, (\varphi \rightarrow x = y) \)
nfxfr l0 _