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

Proof

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

Metamath Proof Explorer

Theorem sb4a

Proof