Theorem mobi

Equivalence theorem for the at-most-one quantifier. (Contributed by BJ, 7-Oct-2022.) (Proof shortened by Wolf Lammen, 18-Feb-2023.)

Conclusion
\( \vdash \forall x \, (\varphi \leftrightarrow \psi) \rightarrow (\exists^\ast x \, \varphi \leftrightarrow \exists^\ast x \, \psi) \)
Proof
l0
albiim
\( \vdash \forall x \, (\varphi \leftrightarrow \psi) \leftrightarrow \forall x \, (\varphi \rightarrow \psi) \wedge \forall x \, (\psi \rightarrow \varphi) \)
l1
moim
moim
impbid21d l1 _
imp _
\( \vdash \forall x \, (\varphi \rightarrow \psi) \wedge \forall x \, (\psi \rightarrow \varphi) \rightarrow (\exists^\ast x \, \varphi \leftrightarrow \exists^\ast x \, \psi) \)
sylbi l0 _