Metamath Proof Explorer

Theorem ax12dgen

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

Ref Expression
Assertion ax12dgen x = x x φ x x = x φ


Step Hyp Ref Expression
1 ala1 x φ x x = x φ
2 1 a1i x = x x φ x x = x φ