Metamath Proof Explorer

Theorem elong

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

Ref Expression
Assertion elong 
|- ( A e. V -> ( A e. On <-> Ord A ) )

Proof

Step Hyp Ref Expression
1 ordeq 
 |-  ( x = A -> ( Ord x <-> Ord A ) )
2 df-on 
 |-  On = { x | Ord x }
3 1 2 elab2g 
 |-  ( A e. V -> ( A e. On <-> Ord A ) )