Metamath Proof Explorer

Theorem wl-sbalnae

Description: A theorem used in elimination of disjoint variable restrictions by replacing them with distinctors. (Contributed by Wolf Lammen, 25-Jul-2019)

Ref Expression
Assertion wl-sbalnae ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → z y ∀ x φ ↔ ∀ x z y φ

Proof

Step Hyp Ref Expression
1 sb4b ⊢ ¬ ∀ y y = z → z y ∀ x φ ↔ ∀ y y = z → ∀ x φ
2 nfnae ⊢ Ⅎ y ¬ ∀ x x = y
3 nfnae ⊢ Ⅎ y ¬ ∀ x x = z
4 2 3 nfan ⊢ Ⅎ y ¬ ∀ x x = y ∧ ¬ ∀ x x = z
5 nfeqf ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x y = z
6 19.21t ⊢ Ⅎ x y = z → ∀ x y = z → φ ↔ y = z → ∀ x φ
7 6 bicomd ⊢ Ⅎ x y = z → y = z → ∀ x φ ↔ ∀ x y = z → φ
8 5 7 syl ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → y = z → ∀ x φ ↔ ∀ x y = z → φ
9 4 8 albid ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → ∀ y y = z → ∀ x φ ↔ ∀ y ∀ x y = z → φ
10 1 9 sylan9bbr ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → z y ∀ x φ ↔ ∀ y ∀ x y = z → φ
11 nfnae ⊢ Ⅎ x ¬ ∀ y y = z
12 sb4b ⊢ ¬ ∀ y y = z → z y φ ↔ ∀ y y = z → φ
13 11 12 albid ⊢ ¬ ∀ y y = z → ∀ x z y φ ↔ ∀ x ∀ y y = z → φ
14 alcom ⊢ ∀ x ∀ y y = z → φ ↔ ∀ y ∀ x y = z → φ
15 13 14 bitrdi ⊢ ¬ ∀ y y = z → ∀ x z y φ ↔ ∀ y ∀ x y = z → φ
16 15 adantl ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → ∀ x z y φ ↔ ∀ y ∀ x y = z → φ
17 10 16 bitr4d ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ ¬ ∀ y y = z → z y ∀ x φ ↔ ∀ x z y φ
18 17 ex ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → ¬ ∀ y y = z → z y ∀ x φ ↔ ∀ x z y φ
19 sbequ12 ⊢ y = z → ∀ x φ ↔ z y ∀ x φ
20 19 sps ⊢ ∀ y y = z → ∀ x φ ↔ z y ∀ x φ
21 sbequ12 ⊢ y = z → φ ↔ z y φ
22 21 sps ⊢ ∀ y y = z → φ ↔ z y φ
23 22 dral2 ⊢ ∀ y y = z → ∀ x φ ↔ ∀ x z y φ
24 20 23 bitr3d ⊢ ∀ y y = z → z y ∀ x φ ↔ ∀ x z y φ
25 18 24 pm2.61d2 ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → z y ∀ x φ ↔ ∀ x z y φ