Theorem eqelsuc

Description: A set belongs to the successor of an equal set. (Contributed by NM, 18-Aug-1994)

	Ref	Expression
Hypothesis	eqelsuc.1	$$⊢A\in \mathrm{V}$$
Assertion	eqelsuc	$$⊢A=B\to A\in \mathrm{suc}B$$

Proof

Step	Hyp	Ref	Expression
1		eqelsuc.1	$$⊢A\in \mathrm{V}$$
2	1	sucid	$$⊢A\in \mathrm{suc}A$$
3		suceq	$$⊢A=B\to \mathrm{suc}A=\mathrm{suc}B$$
4	2 3	eleqtrid	$$⊢A=B\to A\in \mathrm{suc}B$$