Theorem ax11dgen

Degenerate instance of [ax-11] where bundled variables \( x \) and \( y \) have a common substitution. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 13-Apr-2017.)

Conclusion
\( \vdash \forall x \, \forall x \, \varphi \rightarrow \forall x \, \forall x \, \varphi \)
Proof
id