Metamath Proof Explorer


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 )