Theorem axc10

Show that the original axiom [ax-c10] can be derived from ax6 and axc7 (on top of propositional calculus, [ax-gen], and [ax-4] ). See [ax6fromc10] for the rederivation of ax6 from [ax-c10].

Normally, axc10 should be used rather than [ax-c10], except by theorems specifically studying the latter's properties. See [bj-axc10v] for a weaker version requiring fewer axioms. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) Usage of this theorem is discouraged because it depends on [ax-13]. (New usage is discouraged.)

Conclusion
\( \vdash \forall x \, (x = y' \rightarrow \forall x \, \varphi) \rightarrow \varphi \)
Proof
l0
ax6
\( \vdash \neg \forall x \, \neg x = y' \)
con3
al2imi _
\( \vdash \forall x \, (x = y' \rightarrow \forall x \, \varphi) \rightarrow \forall x \, \neg \forall x \, \varphi \rightarrow \forall x \, \neg x = y' \)
l3
mtoi l0 _
\( \vdash \forall x \, (x = y' \rightarrow \forall x \, \varphi) \rightarrow \neg \forall x \, \neg \forall x \, \varphi \)
axc7
\( \vdash \neg \forall x \, \neg \forall x \, \varphi \rightarrow \varphi \)
syl l3 _