Theorem ax12w

Weak version of [ax-12] from which we can prove any [ax-12] instance not involving wff variables or bundling. Uses only Tarski's FOL axiom schemes. An instance of the first hypothesis will normally require that \( x \) and \( y \) be distinct (unless \( x \) does not occur in \( \varphi \) ). For an example of how the hypotheses can be eliminated when we substitute an expression without wff variables for \( \varphi \), see ax12wdemo. (Contributed by NM, 10-Apr-2017.)

Hypotheses
ax12w.1
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
ax12w.2
\( \vdash y = z \rightarrow (\varphi \leftrightarrow \chi) \)
Conclusion
\( \vdash x = y \rightarrow \forall y \, \varphi \rightarrow \forall x \, (x = y \rightarrow \varphi) \)
Proof
ax12w.2
\( \vdash y = z \rightarrow (\varphi \leftrightarrow \chi) \)
l1
spw _
\( \vdash \forall y \, \varphi \rightarrow \varphi \)
ax12w.1
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
ax12wlem _
\( \vdash x = y \rightarrow \varphi \rightarrow \forall x \, (x = y \rightarrow \varphi) \)
syl5 l1 _