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

Metamath Proof Explorer

Theorem sb4av

Description: Version of sb4a with a disjoint variable condition, which does not require ax-13 . The distinctor antecedent from sb4b is replaced by a disjoint variable condition in this theorem. (Contributed by NM, 2-Feb-2007) (Revised by BJ, 15-Dec-2023)

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

Proof

Step	Hyp	Ref	Expression
1		sp	⊢ ( ∀ 𝑡 𝜑 → 𝜑 )
2	1	sbimi	⊢ ( [ 𝑡 / 𝑥 ] ∀ 𝑡 𝜑 → [ 𝑡 / 𝑥 ] 𝜑 )
3		sb6	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜑 ) )
4	2 3	sylib	⊢ ( [ 𝑡 / 𝑥 ] ∀ 𝑡 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜑 ) )