Description: The successor of a set is a set (generalization). (Contributed by NM, 5-Jun-1994)
Ref | Expression | ||
---|---|---|---|
Assertion | sucexg | ⊢ ( 𝐴 ∈ 𝑉 → suc 𝐴 ∈ V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex | ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V ) | |
2 | sucexb | ⊢ ( 𝐴 ∈ V ↔ suc 𝐴 ∈ V ) | |
3 | 1 2 | sylib | ⊢ ( 𝐴 ∈ 𝑉 → suc 𝐴 ∈ V ) |