Theorem ax12v2

It is possible to remove any restriction on \( \varphi \) in ax12v. Same as Axiom C8 of [Monk2] p. 105. Use ax12v instead when sufficient. (Contributed by NM, 5-Aug-1993.) Remove dependencies on [ax-10] and [ax-13]. (Revised by Jim Kingdon, 15-Dec-2017.) (Proof shortened by Wolf Lammen, 8-Dec-2019.)

Conclusion
\( \vdash x = y' \rightarrow \varphi \rightarrow \forall x \, (x = y' \rightarrow \varphi) \)
Proof
l0
equtrr
\( \vdash y' = z \rightarrow x = y' \rightarrow x = z \)
l1
ax12v
\( \vdash x = z \rightarrow \varphi \rightarrow \forall x \, (x = z \rightarrow \varphi) \)
imim1d l0
alimdv _
\( \vdash y' = z \rightarrow \forall x \, (x = z \rightarrow \varphi) \rightarrow \forall x \, (x = y' \rightarrow \varphi) \)
syl9r l1 _
\( \vdash y' = z \rightarrow x = z \rightarrow \varphi \rightarrow \forall x \, (x = y' \rightarrow \varphi) \)
l5
syld l0 _
\( \vdash y' = z \rightarrow x = y' \rightarrow \varphi \rightarrow \forall x \, (x = y' \rightarrow \varphi) \)
ax6evr
\( \vdash \exists z \, y' = z \)
exlimiiv l5 _