Metamath Proof Explorer

Theorem elon2

Description: An ordinal number is an ordinal set. (Contributed by NM, 8-Feb-2004)

Ref Expression
Assertion elon2 
|- ( A e. On <-> ( Ord A /\ A e. _V ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. On -> A e. _V )
2 elong 
 |-  ( A e. _V -> ( A e. On <-> Ord A ) )
3 1 2 biadanii 
 |-  ( A e. On <-> ( A e. _V /\ Ord A ) )
4 3 biancomi 
 |-  ( A e. On <-> ( Ord A /\ A e. _V ) )