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

Proof

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