This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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		dfsb	$⊢ [t/ x] φ \leftrightarrow \forall y (y = t \to \forall x (x = y \to φ))$
2	1	biimpi	$⊢ [t/ x] φ \to \forall y (y = t \to \forall x (x = y \to φ))$
3		equvinva	$⊢ x = t \to \exists y (x = y \land t = y)$
4		equcomi	$⊢ t = y \to y = t$
5		sp	$⊢ \forall x (x = y \to φ) \to (x = y \to φ)$
6	4 5	imim12i	$⊢ (y = t \to \forall x (x = y \to φ)) \to (t = y \to (x = y \to φ))$
7	6	impcomd	$⊢ (y = t \to \forall x (x = y \to φ)) \to ((x = y \land t = y) \to φ)$
8	7	aleximi	$⊢ \forall y (y = t \to \forall x (x = y \to φ)) \to (\exists y (x = y \land t = y) \to \exists y φ)$
9	2 3 8	syl2im	$⊢ [t/ x] φ \to (x = t \to \exists y φ)$
10		ax5e	$⊢ \exists y φ \to φ$
11	9 10	syl6com	$⊢ x = t \to ([t/ x] φ \to φ)$