Theorem stdpc4lem

Description: In the case of stdpc4 , rename-sb is derivable from fewer axioms than dfsb . The essential proof step is presented in this lemma. Based on a proof of BJ, 22-Dec-2020. (Contributed by Wolf Lammen, 4-Jun-2026)

	Ref	Expression
Assertion	stdpc4lem	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ala1	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
2	1	a1d	⊢ ( ∀ 𝑥 𝜑 → ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
3	2	alrimiv	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )