Theorem 19.38b

Under a nonfreeness hypothesis, the implication 19.38 can be strengthened to an equivalence. See also 19.38a. (Contributed by BJ, 3-Nov-2021.) (Proof shortened by Wolf Lammen, 9-Jul-2022.)

Conclusion
\( \vdash \Finv x \, \psi \rightarrow (\exists x \, \varphi \rightarrow \forall x \, \psi \leftrightarrow \forall x \, (\varphi \rightarrow \psi)) \)
Proof
l0
19.38
l1
exim
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow \exists x \, \varphi \rightarrow \exists x \, \psi \)
id
nfrd _
\( \vdash \Finv x \, \psi \rightarrow \exists x \, \psi \rightarrow \forall x \, \psi \)
syl9r l1 _
impbid2 l0 _