Theorem sbeqal1

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

	Ref	Expression
Assertion	sbeqal1	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 = 𝑧 ) → 𝑦 = 𝑧 )

Proof

Step	Hyp	Ref	Expression
1		sb2	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 = 𝑧 ) → [ 𝑦 / 𝑥 ] 𝑥 = 𝑧 )
2		equsb3	⊢ ( [ 𝑦 / 𝑥 ] 𝑥 = 𝑧 ↔ 𝑦 = 𝑧 )
3	1 2	sylib	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 = 𝑧 ) → 𝑦 = 𝑧 )