Theorem 19.21

Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " \( x \) is not free in \( \varphi \) ". See 19.21v for a version requiring fewer axioms. See also 19.21h. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) [df-nf] changed. (Revised by Wolf Lammen, 18-Sep-2021.)

Hypothesis
19.21.1
\( \vdash \Finv x \, \varphi \)
Conclusion
\( \vdash \forall x \, (\varphi \rightarrow \psi) \leftrightarrow \varphi \rightarrow \forall x \, \psi \)
Proof
l0
19.21.1
\( \vdash \Finv x \, \varphi \)
19.21t
\( \vdash \Finv x \, \varphi \rightarrow (\forall x \, (\varphi \rightarrow \psi) \leftrightarrow \varphi \rightarrow \forall x \, \psi) \)
ax-mp l0 _