Metamath Proof Explorer

Theorem wl-ax13lem1

Description: A version of ax-wl-13v with one distinct variable restriction dropped. For convenience, y is kept on the right side of equations. This proof bases on ideas from NM, 24-Dec-2015. (Contributed by Wolf Lammen, 23-Jul-2021)

Ref Expression
Assertion wl-ax13lem1 
|- ( -. A. x x = y -> ( z = y -> A. x z = y ) )

Proof

Step Hyp Ref Expression
1 equvinva 
 |-  ( z = y -> E. w ( z = w /\ y = w ) )
2 ax-wl-13v 
 |-  ( -. A. x x = y -> ( y = w -> A. x y = w ) )
3 equeucl 
 |-  ( z = w -> ( y = w -> z = y ) )
4 3 alimdv 
 |-  ( z = w -> ( A. x y = w -> A. x z = y ) )
5 2 4 syl9 
 |-  ( -. A. x x = y -> ( z = w -> ( y = w -> A. x z = y ) ) )
6 5 impd 
 |-  ( -. A. x x = y -> ( ( z = w /\ y = w ) -> A. x z = y ) )
7 6 exlimdv 
 |-  ( -. A. x x = y -> ( E. w ( z = w /\ y = w ) -> A. x z = y ) )
8 1 7 syl5 
 |-  ( -. A. x x = y -> ( z = y -> A. x z = y ) )