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