Metamath Proof Explorer

Theorem omsucelsucb

Description: Membership is inherited by successors for natural numbers. (Contributed by AV, 15-Sep-2023)

Ref Expression
Assertion omsucelsucb 
|- ( N e. _om <-> suc N e. suc _om )

Proof

Step Hyp Ref Expression
1 ordom 
 |-  Ord _om
2 ordsucelsuc 
 |-  ( Ord _om -> ( N e. _om <-> suc N e. suc _om ) )
3 1 2 ax-mp 
 |-  ( N e. _om <-> suc N e. suc _om )