Description: Degenerate instance of ax-13 where bundled variables x and z have a common substitution. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 13-Apr-2017)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax13dgen2 | |- ( -. x = y -> ( y = x -> A. x y = x ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | equcomi | |- ( y = x -> x = y ) |
|
| 2 | pm2.21 | |- ( -. x = y -> ( x = y -> A. x y = x ) ) |
|
| 3 | 1 2 | syl5 | |- ( -. x = y -> ( y = x -> A. x y = x ) ) |