Theorem sb4a

Description: A version of one implication of sb4b that does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker sb4av when possible. (Contributed by NM, 2-Feb-2007) Revise df-sb . (Revised by Wolf Lammen, 28-Jul-2023) (New usage is discouraged.)

	Ref	Expression
Assertion	sb4a	$$⊢\left[t/x\right]\forall t\phi \to \forall x\left(x=t\to \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbequ2	$$⊢x=t\to \left(\left[t/x\right]\forall t\phi \to \forall t\phi \right)$$
2	1	sps	$$⊢\forall xx=t\to \left(\left[t/x\right]\forall t\phi \to \forall t\phi \right)$$
3		axc11r	$$⊢\forall xx=t\to \left(\forall t\phi \to \forall x\phi \right)$$
4		ala1	$$⊢\forall x\phi \to \forall x\left(x=t\to \phi \right)$$
5	3 4	syl6	$$⊢\forall xx=t\to \left(\forall t\phi \to \forall x\left(x=t\to \phi \right)\right)$$
6	2 5	syld	$$⊢\forall xx=t\to \left(\left[t/x\right]\forall t\phi \to \forall x\left(x=t\to \phi \right)\right)$$
7		sb4b	$$⊢\neg \forall xx=t\to \left(\left[t/x\right]\forall t\phi \leftrightarrow \forall x\left(x=t\to \forall t\phi \right)\right)$$
8		sp	$$⊢\forall t\phi \to \phi$$
9	8	imim2i	$$⊢\left(x=t\to \forall t\phi \right)\to \left(x=t\to \phi \right)$$
10	9	alimi	$$⊢\forall x\left(x=t\to \forall t\phi \right)\to \forall x\left(x=t\to \phi \right)$$
11	7 10	biimtrdi	$$⊢\neg \forall xx=t\to \left(\left[t/x\right]\forall t\phi \to \forall x\left(x=t\to \phi \right)\right)$$
12	6 11	pm2.61i	$$⊢\left[t/x\right]\forall t\phi \to \forall x\left(x=t\to \phi \right)$$