Theorem 19.38a

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

Conclusion
\( \vdash \Finv x \, \varphi \rightarrow (\exists x \, \varphi \rightarrow \forall x \, \psi \leftrightarrow \forall x \, (\varphi \rightarrow \psi)) \)
Proof
l0
19.38
id
l2
nfrd _
\( \vdash \Finv x \, \varphi \rightarrow \exists x \, \varphi \rightarrow \forall x \, \varphi \)
alim
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow \forall x \, \varphi \rightarrow \forall x \, \psi \)
syl9 l2 _
impbid2 l0 _