Metamath Proof Explorer

Theorem wl-ax11-lem1

Description: A transitive law for variable identifying expressions. (Contributed by Wolf Lammen, 30-Jun-2019)

Ref Expression
Assertion wl-ax11-lem1 ⊢ ∀ x x = y → ∀ x x = z ↔ ∀ y y = z

Proof

Step Hyp Ref Expression
1 wl-aetr ⊢ ∀ x x = y → ∀ x x = z → ∀ y y = z
2 wl-aetr ⊢ ∀ y y = x → ∀ y y = z → ∀ x x = z
3 2 aecoms ⊢ ∀ x x = y → ∀ y y = z → ∀ x x = z
4 1 3 impbid ⊢ ∀ x x = y → ∀ x x = z ↔ ∀ y y = z