Metamath Proof Explorer

Theorem sbeqal1

Description: If x = y always implies x = z , then y = z . (Contributed by Andrew Salmon, 2-Jun-2011)

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

Proof

Step Hyp Ref Expression
1 sb2 
 |-  ( A. x ( x = y -> x = z ) -> [ y / x ] x = z )
2 equsb3 
 |-  ( [ y / x ] x = z <-> y = z )
3 1 2 sylib 
 |-  ( A. x ( x = y -> x = z ) -> y = z )