Metamath Proof Explorer

Theorem ordelss

Description: An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994)

Ref Expression
Assertion ordelss Ord A B A B A


Step Hyp Ref Expression
1 ordtr Ord A Tr A
2 trss Tr A B A B A
3 2 imp Tr A B A B A
4 1 3 sylan Ord A B A B A