sb4b

Description: Simplified definition of substitution when variables are distinct. Version of sb6 with a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 27-May-1997) Revise df-sb . (Revised by Wolf Lammen, 21-Feb-2024) (New usage is discouraged.)

		Ref	Expression
	Assertion	sb4b	$⊢ \neg \forall x x = t \to ([t/ x] φ \leftrightarrow \forall x (x = t \to φ))$

Proof

Step	Hyp	Ref	Expression
1		nfna1	$⊢ Ⅎ x \neg \forall x x = t$
2		nfeqf2	$⊢ \neg \forall x x = t \to Ⅎ x y = t$
3	1 2	nfan1	$⊢ Ⅎ x (\neg \forall x x = t \land y = t)$
4		equequ2	$⊢ y = t \to (x = y \leftrightarrow x = t)$
5	4	imbi1d	$⊢ y = t \to ((x = y \to φ) \leftrightarrow (x = t \to φ))$
6	5	adantl	$⊢ (\neg \forall x x = t \land y = t) \to ((x = y \to φ) \leftrightarrow (x = t \to φ))$
7	3 6	albid	$⊢ (\neg \forall x x = t \land y = t) \to (\forall x (x = y \to φ) \leftrightarrow \forall x (x = t \to φ))$
8	7	pm5.74da	$⊢ \neg \forall x x = t \to ((y = t \to \forall x (x = y \to φ)) \leftrightarrow (y = t \to \forall x (x = t \to φ)))$
9	8	albidv	$⊢ \neg \forall x x = t \to (\forall y (y = t \to \forall x (x = y \to φ)) \leftrightarrow \forall y (y = t \to \forall x (x = t \to φ)))$
10		df-sb	$⊢ [t/ x] φ \leftrightarrow \forall y (y = t \to \forall x (x = y \to φ))$
11		ax6ev	$⊢ \exists y y = t$
12	11	a1bi	$⊢ \forall x (x = t \to φ) \leftrightarrow (\exists y y = t \to \forall x (x = t \to φ))$
13		19.23v	$⊢ \forall y (y = t \to \forall x (x = t \to φ)) \leftrightarrow (\exists y y = t \to \forall x (x = t \to φ))$
14	12 13	bitr4i	$⊢ \forall x (x = t \to φ) \leftrightarrow \forall y (y = t \to \forall x (x = t \to φ))$
15	9 10 14	3bitr4g	$⊢ \neg \forall x x = t \to ([t/ x] φ \leftrightarrow \forall x (x = t \to φ))$

Metamath Proof Explorer

Theorem sb4b

Proof