Theorem dfsbimp

Description: A simple consequence of df-sb . (Contributed by Wolf Lammen, 4-Jun-2026)

	Ref	Expression
Assertion	dfsbimp	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 → ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-sb	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 ↔ ( ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ∧ ∀ 𝑧 ( 𝑧 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )
2	1	simplbi	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 → ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )