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 ( ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) ↔ ∀ 𝑧 ( 𝑧 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑧𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 equequ1 ( 𝑦 = 𝑧 → ( 𝑦 = 𝑡𝑧 = 𝑡 ) )
2 equequ2 ( 𝑦 = 𝑧 → ( 𝑥 = 𝑦𝑥 = 𝑧 ) )
3 2 imbi1d ( 𝑦 = 𝑧 → ( ( 𝑥 = 𝑦𝜑 ) ↔ ( 𝑥 = 𝑧𝜑 ) ) )
4 3 albidv ( 𝑦 = 𝑧 → ( ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑧𝜑 ) ) )
5 1 4 imbi12d ( 𝑦 = 𝑧 → ( ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) ↔ ( 𝑧 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑧𝜑 ) ) ) )
6 5 cbvalvw ( ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) ↔ ∀ 𝑧 ( 𝑧 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑧𝜑 ) ) )