Description: Version of ax-11 with distinct variable conditions. Currently implemented as an axiom to detect unintended references to the foundational axiom ax-11 . It will later be converted into a theorem directly based on ax-11 . (Contributed by Wolf Lammen, 28-Jun-2019)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax-wl-11v | |- ( A. x A. y ph -> A. y A. x ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vx | |- x |
|
| 1 | vy | |- y |
|
| 2 | wph | |- ph |
|
| 3 | 2 1 | wal | |- A. y ph |
| 4 | 3 0 | wal | |- A. x A. y ph |
| 5 | 2 0 | wal | |- A. x ph |
| 6 | 5 1 | wal | |- A. y A. x ph |
| 7 | 4 6 | wi | |- ( A. x A. y ph -> A. y A. x ph ) |