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

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

Proof

Step Hyp Ref Expression
1 dfsb ⊢ ( [ 𝑥 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
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 ⊢ ( [ 𝑥 / 𝑥 ] 𝜑 → 𝜑 )