This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ax13lem2

Description: Lemma for nfeqf2 . This lemma is equivalent to ax13v with one distinct variable constraint removed. (Contributed by Wolf Lammen, 8-Sep-2018) Reduce axiom usage. (Revised by Wolf Lammen, 18-Oct-2020) (New usage is discouraged.)

Ref Expression
Assertion ax13lem2 
|- ( -. x = y -> ( E. x z = y -> z = y ) )

Proof

Step Hyp Ref Expression
1 ax13lem1 
 |-  ( -. x = y -> ( w = y -> A. x w = y ) )
2 equeucl 
 |-  ( z = y -> ( w = y -> z = w ) )
3 2 eximi 
 |-  ( E. x z = y -> E. x ( w = y -> z = w ) )
4 19.36v 
 |-  ( E. x ( w = y -> z = w ) <-> ( A. x w = y -> z = w ) )
5 3 4 sylib 
 |-  ( E. x z = y -> ( A. x w = y -> z = w ) )
6 1 5 syl9 
 |-  ( -. x = y -> ( E. x z = y -> ( w = y -> z = w ) ) )
7 6 alrimdv 
 |-  ( -. x = y -> ( E. x z = y -> A. w ( w = y -> z = w ) ) )
8 equequ2 
 |-  ( w = y -> ( z = w <-> z = y ) )
9 8 equsalvw 
 |-  ( A. w ( w = y -> z = w ) <-> z = y )
10 7 9 imbitrdi 
 |-  ( -. x = y -> ( E. x z = y -> z = y ) )