Theorem sbi1lem

Description: Lemma for sbi1 . The core of the proof was extracted from a proof of SN. (Contributed by Wolf Lammen, 5-Jun-2026)

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

Proof

Step	Hyp	Ref	Expression
1		dfsbimp	⊢ ( [ 𝑡 / 𝑥 ] ( 𝜑 → 𝜓 ) → ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) ) ) )
2		dfsbimp	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 → ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
3		ax-2	⊢ ( ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) ) → ( ( 𝑥 = 𝑦 → 𝜑 ) → ( 𝑥 = 𝑦 → 𝜓 ) ) )
4	3	al2imi	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) ) → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜓 ) ) )
5	4	imim3i	⊢ ( ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) ) ) → ( ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) → ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜓 ) ) ) )
6	5	al2imi	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) ) ) → ( ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) → ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜓 ) ) ) )
7	1 2 6	syl2im	⊢ ( [ 𝑡 / 𝑥 ] ( 𝜑 → 𝜓 ) → ( [ 𝑡 / 𝑥 ] 𝜑 → ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜓 ) ) ) )
8	7	imp	⊢ ( ( [ 𝑡 / 𝑥 ] ( 𝜑 → 𝜓 ) ∧ [ 𝑡 / 𝑥 ] 𝜑 ) → ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜓 ) ) )