Metamath Proof Explorer

Theorem sucex

Description: The successor of a set is a set. (Contributed by NM, 30-Aug-1993)

Ref Expression
Hypothesis sucex.1 
|- A e. _V
Assertion sucex 
|- suc A e. _V

Proof

Step Hyp Ref Expression
1 sucex.1 
 |-  A e. _V
2 sucexg 
 |-  ( A e. _V -> suc A e. _V )
3 1 2 ax-mp 
 |-  suc A e. _V