Metamath Proof Explorer

Theorem peano2b

Description: A class belongs to omega iff its successor does. (Contributed by NM, 3-Dec-1995)

Ref Expression
Assertion peano2b 
|- ( A e. _om <-> suc A e. _om )

Proof

Step Hyp Ref Expression
1 limom 
 |-  Lim _om
2 limsuc 
 |-  ( Lim _om -> ( A e. _om <-> suc A e. _om ) )
3 1 2 ax-mp 
 |-  ( A e. _om <-> suc A e. _om )