Theorem ax12
Rederivation of Axiom [ax-12] from ax12v (used only via sp ),
axc11r, and axc15 (on top of Tarski's FOL). Since this version
depends on [ax-13], usage of the weaker ax12v, ax12w, ax12i are
preferred. (Contributed by NM, 22-Jan-2007.) Proof uses contemporary
axioms. (Revised by Wolf Lammen, 8-Aug-2020.) (Proof shortened by BJ,
4-Jul-2021.) (New usage is discouraged.)
Conclusion
\( \vdash x = y \rightarrow \forall y \, \varphi \rightarrow \forall x \, (x = y \rightarrow \varphi) \)
Proof
l0
axc11r
\( \vdash \forall x \, x = y \rightarrow \forall y \, \varphi \rightarrow \forall x \, \varphi \)
ala1
\( \vdash \forall x \, \varphi \rightarrow \forall x \, (x = y \rightarrow \varphi) \)
syl6 l0 _
l3
a1d _
\( \vdash \forall x \, x = y \rightarrow x = y \rightarrow \forall y \, \varphi \rightarrow \forall x \, (x = y \rightarrow \varphi) \)
l4
sp
\( \vdash \forall y \, \varphi \rightarrow \varphi \)
axc15
\( \vdash \neg \forall x \, x = y \rightarrow x = y \rightarrow \varphi \rightarrow \forall x \, (x = y \rightarrow \varphi) \)
syl7 l4 _
\( \vdash \neg \forall x \, x = y \rightarrow x = y \rightarrow \forall y \, \varphi \rightarrow \forall x \, (x = y \rightarrow \varphi) \)
pm2.61i l3 _