Theorem stdpc4ALT

Description: Alternate proof of stdpc4 , shorter but using additional axioms. (Contributed by WL, 5-Jun-2026) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	stdpc4ALT	⊢ ( ∀ 𝑥 𝜑 → [ 𝑡 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		ala1	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
2	1	a1d	⊢ ( ∀ 𝑥 𝜑 → ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
3	2	alrimiv	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
4		dfsb	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
5	3 4	sylibr	⊢ ( ∀ 𝑥 𝜑 → [ 𝑡 / 𝑥 ] 𝜑 )