Metamath Proof Explorer

Theorem eloni

Description: An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994)

Ref Expression
Assertion eloni 
|- ( A e. On -> Ord A )

Proof

Step Hyp Ref Expression
1 elong 
 |-  ( A e. On -> ( A e. On <-> Ord A ) )
2 1 ibi 
 |-  ( A e. On -> Ord A )