Metamath Proof Explorer


Theorem wl-ax11-lem9

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 ) )

Proof

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 ) )