An equivalence between an implication with a universally quantified
consequent and an implication with an existentially quantified antecedent.
An interesting case is when the same formula is substituted for both
\( \varphi \) and \( \psi \), since then both implications express a type of
nonfreeness. See also eximal. (Contributed by BJ, 12-May-2019.)
\( \vdash \varphi \rightarrow \forall x \, \psi \leftrightarrow \exists x \, \neg \psi \rightarrow \neg \varphi \)
\( \vdash \varphi \rightarrow \forall x \, \psi \leftrightarrow \varphi \rightarrow \neg \exists x \, \neg \psi \)
\( \vdash \varphi \rightarrow \neg \exists x \, \neg \psi \leftrightarrow \exists x \, \neg \psi \rightarrow \neg \varphi \)