Theorem eqelsuc

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

	Ref	Expression
Hypothesis	eqelsuc.1	⊢ 𝐴 ∈ V
Assertion	eqelsuc	⊢ ( 𝐴 = 𝐵 → 𝐴 ∈ suc 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eqelsuc.1	⊢ 𝐴 ∈ V
2	1	sucid	⊢ 𝐴 ∈ suc 𝐴
3		suceq	⊢ ( 𝐴 = 𝐵 → suc 𝐴 = suc 𝐵 )
4	2 3	eleqtrid	⊢ ( 𝐴 = 𝐵 → 𝐴 ∈ suc 𝐵 )