Metamath Proof Explorer

Theorem bj-ax6elem1

Description: Lemma for bj-ax6e . (Contributed by BJ, 22-Dec-2020) (Proof modification is discouraged.)

Ref Expression
Assertion bj-ax6elem1 
|- ( -. A. x x = y -> ( y = z -> A. x y = z ) )

Proof

Step Hyp Ref Expression
1 axc9 
 |-  ( -. A. x x = y -> ( -. A. x x = z -> ( y = z -> A. x y = z ) ) )
2 axc16 
 |-  ( A. x x = z -> ( y = z -> A. x y = z ) )
3 1 2 pm2.61d2 
 |-  ( -. A. x x = y -> ( y = z -> A. x y = z ) )