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	$⊢ [t/ x] \forall t φ \to \forall x (x = t \to φ)$

Proof

Step	Hyp	Ref	Expression
1		sp	$⊢ \forall t φ \to φ$
2	1	sbimi	$⊢ [t/ x] \forall t φ \to [t/ x] φ$
3		sb6	$⊢ [t/ x] φ \leftrightarrow \forall x (x = t \to φ)$
4	2 3	sylib	$⊢ [t/ x] \forall t φ \to \forall x (x = t \to φ)$