Metamath Proof Explorer

Theorem elon

Description: An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994)

Ref Expression
Hypothesis elon.1 
|- A e. _V
Assertion elon 
|- ( A e. On <-> Ord A )

Proof

Step Hyp Ref Expression
1 elon.1 
 |-  A e. _V
2 elong 
 |-  ( A e. _V -> ( A e. On <-> Ord A ) )
3 1 2 ax-mp 
 |-  ( A e. On <-> Ord A )