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	|- A e. V
	eqsucidi.2	|- B = suc A
Assertion	eqsucidi	|- A e. B

Proof

Step	Hyp	Ref	Expression
1		eqsucidi.1	|- A e. V
2		eqsucidi.2	|- B = suc A
3		sucidg	|- ( A e. V -> A e. suc A )
4	1 3	ax-mp	|- A e. suc A
5	4 2	eleqtrri	|- A e. B