This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 V$
	Assertion	eqelsuc	$⊢ A = B \to A \in suc B$

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