Metamath Proof Explorer

Theorem sbequ2OLD

Description: Obsolete version of sbequ2 as of 3-Feb-2024. (Contributed by NM, 16-May-1993) (Proof shortened by Wolf Lammen, 25-Feb-2018) Revise df-sb . (Revised by BJ, 22-Dec-2020) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	sbequ2OLD	$⊢ x = t \to ([t/ x] φ \to φ)$

Proof

Step	Hyp	Ref	Expression
1		equvinva	$⊢ x = t \to \exists y (x = y \land t = y)$
2		df-sb	$⊢ [t/ x] φ \leftrightarrow \forall y (y = t \to \forall x (x = y \to φ))$
3		equcomi	$⊢ t = y \to y = t$
4		sp	$⊢ \forall x (x = y \to φ) \to (x = y \to φ)$
5	3 4	imim12i	$⊢ (y = t \to \forall x (x = y \to φ)) \to (t = y \to (x = y \to φ))$
6	5	impcomd	$⊢ (y = t \to \forall x (x = y \to φ)) \to ((x = y \land t = y) \to φ)$
7	6	alimi	$⊢ \forall y (y = t \to \forall x (x = y \to φ)) \to \forall y ((x = y \land t = y) \to φ)$
8	2 7	sylbi	$⊢ [t/ x] φ \to \forall y ((x = y \land t = y) \to φ)$
9		19.23v	$⊢ \forall y ((x = y \land t = y) \to φ) \leftrightarrow (\exists y (x = y \land t = y) \to φ)$
10	8 9	sylib	$⊢ [t/ x] φ \to (\exists y (x = y \land t = y) \to φ)$
11	1 10	syl5com	$⊢ x = t \to ([t/ x] φ \to φ)$