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

Metamath Proof Explorer

Theorem sb4a

Description: A version of one implication of sb4b that does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker sb4av when possible. (Contributed by NM, 2-Feb-2007) Revise df-sb . (Revised by Wolf Lammen, 28-Jul-2023) (New usage is discouraged.)

Ref Expression
Assertion sb4a ( [ 𝑡 / 𝑥 ] ∀ 𝑡 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜑 ) )

Proof

Step Hyp Ref Expression
1 sbequ2 ⊢ ( 𝑥 = 𝑡 → ( [ 𝑡 / 𝑥 ] ∀ 𝑡 𝜑 → ∀ 𝑡 𝜑 ) )
2 1 sps ⊢ ( ∀ 𝑥 𝑥 = 𝑡 → ( [ 𝑡 / 𝑥 ] ∀ 𝑡 𝜑 → ∀ 𝑡 𝜑 ) )
3 axc11r ⊢ ( ∀ 𝑥 𝑥 = 𝑡 → ( ∀ 𝑡 𝜑 → ∀ 𝑥 𝜑 ) )
4 ala1 ⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜑 ) )
5 3 4 syl6 ⊢ ( ∀ 𝑥 𝑥 = 𝑡 → ( ∀ 𝑡 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜑 ) ) )
6 2 5 syld ⊢ ( ∀ 𝑥 𝑥 = 𝑡 → ( [ 𝑡 / 𝑥 ] ∀ 𝑡 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜑 ) ) )
7 sb4b ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑡 → ( [ 𝑡 / 𝑥 ] ∀ 𝑡 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑡 → ∀ 𝑡 𝜑 ) ) )
8 sp ⊢ ( ∀ 𝑡 𝜑 → 𝜑 )
9 8 imim2i ⊢ ( ( 𝑥 = 𝑡 → ∀ 𝑡 𝜑 ) → ( 𝑥 = 𝑡 → 𝜑 ) )
10 9 alimi ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑡 → ∀ 𝑡 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜑 ) )
11 7 10 biimtrdi ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑡 → ( [ 𝑡 / 𝑥 ] ∀ 𝑡 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜑 ) ) )
12 6 11 pm2.61i ⊢ ( [ 𝑡 / 𝑥 ] ∀ 𝑡 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜑 ) )