Theorem mobii

Formula-building rule for the at-most-one quantifier (inference form). (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.)

Hypothesis
mobii.1
\( \vdash \psi \leftrightarrow \chi \)
Conclusion
\( \vdash \exists^\ast x \, \psi \leftrightarrow \exists^\ast x \, \chi \)
Proof
l0
mobi
\( \vdash \forall x \, (\psi \leftrightarrow \chi) \rightarrow (\exists^\ast x \, \psi \leftrightarrow \exists^\ast x \, \chi) \)
mobii.1
\( \vdash \psi \leftrightarrow \chi \)
mpg l0 _