Description: The easy part when x coincides with y . (Contributed by Wolf Lammen, 30-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | wl-ax11-lem9 | |- ( A. x x = y -> ( A. y A. x ph <-> A. x A. y ph ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biidd | |- ( A. x x = y -> ( ph <-> ph ) ) |
|
2 | 1 | dral1 | |- ( A. x x = y -> ( A. x ph <-> A. y ph ) ) |
3 | 2 | aecoms | |- ( A. y y = x -> ( A. x ph <-> A. y ph ) ) |
4 | 3 | dral1 | |- ( A. y y = x -> ( A. y A. x ph <-> A. x A. y ph ) ) |
5 | 4 | aecoms | |- ( A. x x = y -> ( A. y A. x ph <-> A. x A. y ph ) ) |