Description: Degenerate instance of ax-13 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 | ax13dgen1 | |- ( -. x = x -> ( x = z -> A. x x = z ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | equid | |- x = x |
|
| 2 | 1 | pm2.24i | |- ( -. x = x -> ( x = z -> A. x x = z ) ) |