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 -> ( A. x ph -> A. x ( x = x -> ph ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ala1 | |- ( A. x ph -> A. x ( x = x -> ph ) ) |
|
| 2 | 1 | a1i | |- ( x = x -> ( A. x ph -> A. x ( x = x -> ph ) ) ) |