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	⊢ ( [ 𝑥 / 𝑥 ] 𝜑 → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		df-sb	⊢ ( [ 𝑥 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
2		sp	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ( 𝑥 = 𝑦 → 𝜑 ) )
3	2	imim2i	⊢ ( ( 𝑦 = 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) → ( 𝑦 = 𝑥 → ( 𝑥 = 𝑦 → 𝜑 ) ) )
4	3	alimi	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) → ∀ 𝑦 ( 𝑦 = 𝑥 → ( 𝑥 = 𝑦 → 𝜑 ) ) )
5		pm2.21	⊢ ( ¬ 𝑦 = 𝑥 → ( 𝑦 = 𝑥 → 𝜑 ) )
6		equcomi	⊢ ( 𝑦 = 𝑥 → 𝑥 = 𝑦 )
7	6	imim1i	⊢ ( ( 𝑥 = 𝑦 → 𝜑 ) → ( 𝑦 = 𝑥 → 𝜑 ) )
8	5 7	ja	⊢ ( ( 𝑦 = 𝑥 → ( 𝑥 = 𝑦 → 𝜑 ) ) → ( 𝑦 = 𝑥 → 𝜑 ) )
9	8	alimi	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑥 → ( 𝑥 = 𝑦 → 𝜑 ) ) → ∀ 𝑦 ( 𝑦 = 𝑥 → 𝜑 ) )
10		ax6ev	⊢ ∃ 𝑦 𝑦 = 𝑥
11		19.23v	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑥 → 𝜑 ) ↔ ( ∃ 𝑦 𝑦 = 𝑥 → 𝜑 ) )
12	11	biimpi	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑥 → 𝜑 ) → ( ∃ 𝑦 𝑦 = 𝑥 → 𝜑 ) )
13	9 10 12	mpisyl	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑥 → ( 𝑥 = 𝑦 → 𝜑 ) ) → 𝜑 )
14	4 13	syl	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) → 𝜑 )
15	1 14	sylbi	⊢ ( [ 𝑥 / 𝑥 ] 𝜑 → 𝜑 )