Theorem spvw

Version of sp when \( x \) does not occur in \( \varphi \). Converse of [ax-5]. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 10-Apr-2017.) (Proof shortened by Wolf Lammen, 4-Dec-2017.) Shorten 19.3v. (Revised by Wolf Lammen, 20-Oct-2023.)

Conclusion
\( \vdash \forall x \, \varphi \rightarrow \varphi \)
Proof
ax-5
spnfw _