Theorem bj-ssbid1ALT

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

	Ref	Expression
Assertion	bj-ssbid1ALT	$$⊢\phi \to \left[x/x\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		ax12v	$$⊢x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)$$
2	1	equcoms	$$⊢y=x\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)$$
3	2	com12	$$⊢\phi \to \left(y=x\to \forall x\left(x=y\to \phi \right)\right)$$
4	3	alrimiv	$$⊢\phi \to \forall y\left(y=x\to \forall x\left(x=y\to \phi \right)\right)$$
5		df-sb	$$⊢\left[x/x\right]\phi \leftrightarrow \forall y\left(y=x\to \forall x\left(x=y\to \phi \right)\right)$$
6	4 5	sylibr	$$⊢\phi \to \left[x/x\right]\phi$$