Metamath Proof Explorer

Theorem bj-ssbid2ALT

Description: Alternate proof of bj-ssbid2 , not using sbequ2 . (Contributed by BJ, 22-Dec-2020) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	bj-ssbid2ALT	$⊢ [x/ x] φ \to φ$

Proof

Step	Hyp	Ref	Expression
1		df-sb	$⊢ [x/ x] φ \leftrightarrow \forall y (y = x \to \forall x (x = y \to φ))$
2		sp	$⊢ \forall x (x = y \to φ) \to (x = y \to φ)$
3	2	imim2i	$⊢ (y = x \to \forall x (x = y \to φ)) \to (y = x \to (x = y \to φ))$
4	3	alimi	$⊢ \forall y (y = x \to \forall x (x = y \to φ)) \to \forall y (y = x \to (x = y \to φ))$
5		pm2.21	$⊢ \neg y = x \to (y = x \to φ)$
6		equcomi	$⊢ y = x \to x = y$
7	6	imim1i	$⊢ (x = y \to φ) \to (y = x \to φ)$
8	5 7	ja	$⊢ (y = x \to (x = y \to φ)) \to (y = x \to φ)$
9	8	alimi	$⊢ \forall y (y = x \to (x = y \to φ)) \to \forall y (y = x \to φ)$
10		ax6ev	$⊢ \exists y y = x$
11		19.23v	$⊢ \forall y (y = x \to φ) \leftrightarrow (\exists y y = x \to φ)$
12	11	biimpi	$⊢ \forall y (y = x \to φ) \to (\exists y y = x \to φ)$
13	9 10 12	mpisyl	$⊢ \forall y (y = x \to (x = y \to φ)) \to φ$
14	4 13	syl	$⊢ \forall y (y = x \to \forall x (x = y \to φ)) \to φ$
15	1 14	sylbi	$⊢ [x/ x] φ \to φ$