Metamath Proof Explorer

Theorem onelss

Description: An element of an ordinal number is a subset of the number. (Contributed by NM, 5-Jun-1994) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion onelss A On B A B A


Step Hyp Ref Expression
1 eloni A On Ord A
2 ordelss Ord A B A B A
3 2 ex Ord A B A B A
4 1 3 syl A On B A B A