Metamath Proof Explorer

Theorem sbequ2

Description: An equality theorem for substitution. (Contributed by NM, 16-May-1993) Revise df-sb . (Revised by BJ, 22-Dec-2020) (Proof shortened by Wolf Lammen, 3-Feb-2024)

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

Proof

Step	Hyp	Ref	Expression
1		dfsbimp	$⊢ [t/ x] φ \to \forall y (y = t \to \forall x (x = y \to φ))$
2		equvinva	$⊢ x = t \to \exists y (x = y \land t = y)$
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	aleximi	$⊢ \forall y (y = t \to \forall x (x = y \to φ)) \to (\exists y (x = y \land t = y) \to \exists y φ)$
8	1 2 7	syl2im	$⊢ [t/ x] φ \to (x = t \to \exists y φ)$
9		ax5e	$⊢ \exists y φ \to φ$
10	8 9	syl6com	$⊢ x = t \to ([t/ x] φ \to φ)$