Theorem sucidALT

Description: A set belongs to its successor. This proof was automatically derived from sucidALTVD using translate__without__overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	sucidALT.1	|- A e. _V
Assertion	sucidALT	|- A e. suc A

Proof

Step	Hyp	Ref	Expression
1		sucidALT.1	|- A e. _V
2	1	snid	|- A e. { A }
3		elun1	|- ( A e. { A } -> A e. ( { A } u. A ) )
4	2 3	ax-mp	|- A e. ( { A } u. A )
5		df-suc	|- suc A = ( A u. { A } )
6	5	equncomi	|- suc A = ( { A } u. A )
7	4 6	eleqtrri	|- A e. suc A