This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sb8f

Description: Substitution of variable in universal quantifier. Version of sb8 with a disjoint variable condition, not requiring ax-10 or ax-13 . (Contributed by NM, 16-May-1993) (Revised by Wolf Lammen, 19-Jan-2023) Avoid ax-10 . (Revised by SN, 5-Dec-2024)

Ref Expression
Hypothesis sb8f.nf ⊢ Ⅎ y φ
Assertion sb8f ⊢ ∀ x φ ↔ ∀ y y x φ

Proof

Step Hyp Ref Expression
1 sb8f.nf ⊢ Ⅎ y φ
2 sb6 ⊢ y x φ ↔ ∀ x x = y → φ
3 2 albii ⊢ ∀ y y x φ ↔ ∀ y ∀ x x = y → φ
4 alcom ⊢ ∀ y ∀ x x = y → φ ↔ ∀ x ∀ y x = y → φ
5 sb6 ⊢ x y φ ↔ ∀ y y = x → φ
6 1 sbf ⊢ x y φ ↔ φ
7 equcom ⊢ y = x ↔ x = y
8 7 imbi1i ⊢ y = x → φ ↔ x = y → φ
9 8 albii ⊢ ∀ y y = x → φ ↔ ∀ y x = y → φ
10 5 6 9 3bitr3ri ⊢ ∀ y x = y → φ ↔ φ
11 10 albii ⊢ ∀ x ∀ y x = y → φ ↔ ∀ x φ
12 3 4 11 3bitrri ⊢ ∀ x φ ↔ ∀ y y x φ