Theorem ax12wlem

Lemma for weak version of [ax-12]. Uses only Tarski's FOL axiom schemes. In some cases, this lemma may lead to shorter proofs than ax12w. (Contributed by NM, 10-Apr-2017.)

Hypothesis
ax12wlemw.1
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash x = y' \rightarrow \varphi \rightarrow \forall x \, (x = y' \rightarrow \varphi) \)
Proof
l0
ax12wlemw.1
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
ax-5
\( \vdash \psi \rightarrow \forall x \, \psi \)
ax12i l0 _