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

Metamath Proof Explorer

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	⊢ 𝐴 ∈ V
	Assertion	sucidALT	⊢ 𝐴 ∈ suc 𝐴

Proof

Step	Hyp	Ref	Expression
1		sucidALT.1	⊢ 𝐴 ∈ V
2	1	snid	⊢ 𝐴 ∈ { 𝐴 }
3		elun1	⊢ ( 𝐴 ∈ { 𝐴 } → 𝐴 ∈ ( { 𝐴 } ∪ 𝐴 ) )
4	2 3	ax-mp	⊢ 𝐴 ∈ ( { 𝐴 } ∪ 𝐴 )
5		df-suc	⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
6	5	equncomi	⊢ suc 𝐴 = ( { 𝐴 } ∪ 𝐴 )
7	4 6	eleqtrri	⊢ 𝐴 ∈ suc 𝐴