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 ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) )

Proof

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