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	$$⊢\left[x/x\right]\phi \to \phi$$

Proof

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