Metamath Proof Explorer

Theorem sb4bOLD

Description: Obsolete version of sb4b as of 21-Feb-2024. (Contributed by NM, 27-May-1997) Revise df-sb . (Revised by Wolf Lammen, 25-Jul-2023) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

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