Metamath Proof Explorer


Theorem wl-speqv

Description: Under the assumption -. x = y a specialized version of sp is provable from Tarski's FOL and ax13v only. Note that this reverts the implication in ax13lem1 , so in fact ( -. x = y -> ( A. x z = y <-> z = y ) ) holds. (Contributed by Wolf Lammen, 17-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 19.2
 |-  ( A. x z = y -> E. x z = y )
2 ax13lem2
 |-  ( -. x = y -> ( E. x z = y -> z = y ) )
3 1 2 syl5
 |-  ( -. x = y -> ( A. x z = y -> z = y ) )