Metamath Proof Explorer

Theorem sbal2OLD

Description: Obsolete version of sbal2 as of 23-Sep-2023. (Contributed by NM, 2-Jan-2002) Remove a distinct variable constraint. (Revised by Wolf Lammen, 24-Dec-2022) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sbal2OLD ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) )

Proof

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