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 
 |-  ( y = x -> ( Ord y <-> Ord x ) )
2 ordeq 
 |-  ( x = A -> ( Ord x <-> Ord A ) )
3 df-on 
 |-  On = { y | Ord y }
4 1 2 3 elab2gw 
 |-  ( A e. V -> ( A e. On <-> Ord A ) )