Metamath Proof Explorer

Theorem wl-aleq

Description: The semantics of A. x y = z . (Contributed by Wolf Lammen, 27-Apr-2018)

Ref Expression
Assertion wl-aleq ⊢ ∀ x y = z ↔ y = z ∧ ∀ x x = y ↔ ∀ x x = z

Proof

Step Hyp Ref Expression
1 sp ⊢ ∀ x y = z → y = z
2 equequ2 ⊢ y = z → x = y ↔ x = z
3 2 alimi ⊢ ∀ x y = z → ∀ x x = y ↔ x = z
4 albi ⊢ ∀ x x = y ↔ x = z → ∀ x x = y ↔ ∀ x x = z
5 3 4 syl ⊢ ∀ x y = z → ∀ x x = y ↔ ∀ x x = z
6 1 5 jca ⊢ ∀ x y = z → y = z ∧ ∀ x x = y ↔ ∀ x x = z
7 ax7 ⊢ x = y → x = z → y = z
8 7 al2imi ⊢ ∀ x x = y → ∀ x x = z → ∀ x y = z
9 8 a1dd ⊢ ∀ x x = y → ∀ x x = z → y = z → ∀ x y = z
10 axc9 ⊢ ¬ ∀ x x = y → ¬ ∀ x x = z → y = z → ∀ x y = z
11 9 10 bija ⊢ ∀ x x = y ↔ ∀ x x = z → y = z → ∀ x y = z
12 11 impcom ⊢ y = z ∧ ∀ x x = y ↔ ∀ x x = z → ∀ x y = z
13 6 12 impbii ⊢ ∀ x y = z ↔ y = z ∧ ∀ x x = y ↔ ∀ x x = z