Theorem spw

Weak version of the specialization scheme sp. Lemma 9 of [KalishMontague] p. 87. While it appears that sp in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp having mutually distinct setvar variables and no wff metavariables (see ax12wdemo for an example of the procedure to eliminate the hypothesis). Other approximations of sp are spfw (minimal distinct variable requirements), spnfw (when \( x \) is not free in \( \neg \varphi \) ), spvw (when \( x \) does not appear in \( \varphi \) ), sptruw (when \( \varphi \) is true), spfalw (when \( \varphi \) is false), and spvv (where \( \varphi \) is changed into \( \psi \) ). (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 27-Feb-2018.)

Hypothesis
spw.1
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \varphi \)
Proof
l0
ax-5
\( \vdash \neg \psi \rightarrow \forall x \, \neg \psi \)
l1
ax-5
\( \vdash \forall x \, \varphi \rightarrow \forall y \, \forall x \, \varphi \)
l2
ax-5
\( \vdash \neg \varphi \rightarrow \forall y \, \neg \varphi \)
spw.1
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
spfw l0 l1 l2 _