Theorem moim
The at-most-one quantifier reverses implication. (Contributed by NM,
22-Apr-1995.)
Conclusion
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow \exists^\ast x \, \psi \rightarrow \exists^\ast x \, \varphi \)
Proof
imim1
al2imi _
l2
eximdv _
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow \exists y \, \forall x \, (\psi \rightarrow x = y) \rightarrow \exists y \, \forall x \, (\varphi \rightarrow x = y) \)
l3
dfmo
\( \vdash \exists^\ast x \, \psi \leftrightarrow \exists y \, \forall x \, (\psi \rightarrow x = y) \)
dfmo
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists y \, \forall x \, (\varphi \rightarrow x = y) \)
3imtr4g l2 l3 _