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 ⊢ ¬ ∀ x x = y → z y ∀ x φ ↔ ∀ x z y φ

Proof

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