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\in V$$
	eqsucidi.2	$$⊢B=\mathrm{suc}A$$
Assertion	eqsucidi	$$⊢A\in B$$

Proof

Step	Hyp	Ref	Expression
1		eqsucidi.1	$$⊢A\in V$$
2		eqsucidi.2	$$⊢B=\mathrm{suc}A$$
3		sucidg	$$⊢A\in V\to A\in \mathrm{suc}A$$
4	1 3	ax-mp	$$⊢A\in \mathrm{suc}A$$
5	4 2	eleqtrri	$$⊢A\in B$$