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

Metamath Proof Explorer

Theorem sbjust

Description: Justification theorem for df-sb proved from Tarski's FOL axiom schemes. (Contributed by BJ, 22-Jan-2023)

Ref Expression
Assertion sbjust ⊢ ∀ y y = t → ∀ x x = y → φ ↔ ∀ z z = t → ∀ x x = z → φ

Proof

Step Hyp Ref Expression
1 equequ1 ⊢ y = z → y = t ↔ z = t
2 equequ2 ⊢ y = z → x = y ↔ x = z
3 2 imbi1d ⊢ y = z → x = y → φ ↔ x = z → φ
4 3 albidv ⊢ y = z → ∀ x x = y → φ ↔ ∀ x x = z → φ
5 1 4 imbi12d ⊢ y = z → y = t → ∀ x x = y → φ ↔ z = t → ∀ x x = z → φ
6 5 cbvalvw ⊢ ∀ y y = t → ∀ x x = y → φ ↔ ∀ z z = t → ∀ x x = z → φ