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\in \mathrm{V}$$
Assertion	sucidALT	$$⊢A\in \mathrm{suc}A$$

Proof

Step	Hyp	Ref	Expression
1		sucidALT.1	$$⊢A\in \mathrm{V}$$
2	1	snid	$$⊢A\in \left\{A\right\}$$
3		elun1	$$⊢A\in \left\{A\right\}\to A\in \left(\left\{A\right\}\cup A\right)$$
4	2 3	ax-mp	$$⊢A\in \left(\left\{A\right\}\cup A\right)$$
5		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
6	5	equncomi	$$⊢\mathrm{suc}A=\left\{A\right\}\cup A$$
7	4 6	eleqtrri	$$⊢A\in \mathrm{suc}A$$