Theorem sucexg

Description: The successor of a set is a set (generalization). (Contributed by NM, 5-Jun-1994)

	Ref	Expression
Assertion	sucexg	$$⊢A\in V\to \mathrm{suc}A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in V\to A\in \mathrm{V}$$
2		sucexb	$$⊢A\in \mathrm{V}\leftrightarrow \mathrm{suc}A\in \mathrm{V}$$
3	1 2	sylib	$$⊢A\in V\to \mathrm{suc}A\in \mathrm{V}$$