Theorem eqsucidi

Description: A set belongs to its successor. Inference form of sucidg with an equality hypothesis. (Contributed by BTernaryTau, 19-Oct-2026)

	Ref	Expression
Hypotheses	eqsucidi.1	⊢ 𝐴 ∈ 𝑉
	eqsucidi.2	⊢ 𝐵 = suc 𝐴
Assertion	eqsucidi	⊢ 𝐴 ∈ 𝐵

Proof

Step	Hyp	Ref	Expression
1		eqsucidi.1	⊢ 𝐴 ∈ 𝑉
2		eqsucidi.2	⊢ 𝐵 = suc 𝐴
3		sucidg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴 )
4	1 3	ax-mp	⊢ 𝐴 ∈ suc 𝐴
5	4 2	eleqtrri	⊢ 𝐴 ∈ 𝐵