Metamath Proof Explorer

Theorem bj-ax6elem2

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

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

Proof

Step Hyp Ref Expression
1 ax6ev 
 |-  E. x x = z
2 equeucl 
 |-  ( x = z -> ( y = z -> x = y ) )
3 1 2 eximii 
 |-  E. x ( y = z -> x = y )
4 3 19.35i 
 |-  ( A. x y = z -> E. x x = y )