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 e. A ) -> B C_ A )

Proof

Step Hyp Ref Expression
1 ordtr 
 |-  ( Ord A -> Tr A )
2 trss 
 |-  ( Tr A -> ( B e. A -> B C_ A ) )
3 2 imp 
 |-  ( ( Tr A /\ B e. A ) -> B C_ A )
4 1 3 sylan 
 |-  ( ( Ord A /\ B e. A ) -> B C_ A )