Theorem ax6dgen

Tarski's system uses the weaker ax6v instead of the bundled [ax-6], so here we show that the degenerate case of [ax-6] can be derived. Even though [ax-6] is in the list of axioms used, recall that in set.mm, the only statement referencing [ax-6] is ax6v. We later rederive from ax6v the bundled form as ax6 with the help of the auxiliary axiom schemes. (Contributed by NM, 23-Apr-2017.)

Conclusion
\( \vdash \neg \forall x \, \neg x = x \)
Proof
l0
equid
\( \vdash x = x \)
notnoti _
spfalw _
\( \vdash \forall x \, \neg x = x \rightarrow \neg x = x \)
mt2 l0 _