Metamath Proof Explorer

Theorem 0elsuc

Description: The successor of an ordinal class contains the empty set. (Contributed by NM, 4-Apr-1995)

Ref Expression
Assertion 0elsuc 
|- ( Ord A -> (/) e. suc A )

Proof

Step Hyp Ref Expression
1 ordsuc 
 |-  ( Ord A <-> Ord suc A )
2 nsuceq0 
 |-  suc A =/= (/)
3 ord0eln0 
 |-  ( Ord suc A -> ( (/) e. suc A <-> suc A =/= (/) ) )
4 2 3 mpbiri 
 |-  ( Ord suc A -> (/) e. suc A )
5 1 4 sylbi 
 |-  ( Ord A -> (/) e. suc A )