Theorem sucexg

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

	Ref	Expression
Assertion	sucexg	⊢ ( 𝐴 ∈ 𝑉 → suc 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2		sucexb	⊢ ( 𝐴 ∈ V ↔ suc 𝐴 ∈ V )
3	1 2	sylib	⊢ ( 𝐴 ∈ 𝑉 → suc 𝐴 ∈ V )