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	syl6bi	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑡 → ( [ 𝑡 / 𝑥 ] ∀ 𝑡 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜑 ) ) )
12	6 11	pm2.61i	⊢ ( [ 𝑡 / 𝑥 ] ∀ 𝑡 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜑 ) )