Metamath Proof Explorer

Theorem sbal2

Description: Move quantifier in and out of substitution. Usage of this theorem is discouraged because it depends on ax-13 . Check out sbal for a version replacing the distinctor with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 2-Jan-2002) Remove a distinct variable constraint. (Revised by Wolf Lammen, 24-Dec-2022) (Proof shortened by Wolf Lammen, 23-Sep-2023) (New usage is discouraged.)

Ref Expression
Assertion sbal2 ⊢ ¬ ∀ x x = y → z y ∀ x φ ↔ ∀ x z y φ

Proof

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