Metamath Proof Explorer

Theorem wl-ax11-lem6

Description: Lemma. (Contributed by Wolf Lammen, 30-Jun-2019)

Ref Expression
Assertion wl-ax11-lem6 ⊢ ∀ u u = y ∧ ¬ ∀ x x = y → ∀ u ∀ x u y φ ↔ ∀ x ∀ y φ

Proof

Step Hyp Ref Expression
1 ax-wl-11v ⊢ ∀ u ∀ x u y φ → ∀ x ∀ u u y φ
2 ax-wl-11v ⊢ ∀ x ∀ u u y φ → ∀ u ∀ x u y φ
3 1 2 impbii ⊢ ∀ u ∀ x u y φ ↔ ∀ x ∀ u u y φ
4 nfna1 ⊢ Ⅎ x ¬ ∀ x x = y
5 wl-ax11-lem3 ⊢ ¬ ∀ x x = y → Ⅎ x ∀ u u = y
6 4 5 nfan1 ⊢ Ⅎ x ¬ ∀ x x = y ∧ ∀ u u = y
7 wl-ax11-lem5 ⊢ ∀ u u = y → ∀ u u y φ ↔ ∀ y φ
8 7 adantl ⊢ ¬ ∀ x x = y ∧ ∀ u u = y → ∀ u u y φ ↔ ∀ y φ
9 6 8 albid ⊢ ¬ ∀ x x = y ∧ ∀ u u = y → ∀ x ∀ u u y φ ↔ ∀ x ∀ y φ
10 9 ancoms ⊢ ∀ u u = y ∧ ¬ ∀ x x = y → ∀ x ∀ u u y φ ↔ ∀ x ∀ y φ
11 3 10 syl5bb ⊢ ∀ u u = y ∧ ¬ ∀ x x = y → ∀ u ∀ x u y φ ↔ ∀ x ∀ y φ