Metamath Proof Explorer

Theorem onsseleq

Description: Relationship between subset and membership of an ordinal number. (Contributed by NM, 15-Sep-1995)

Ref Expression
Assertion onsseleq 
|- ( ( A e. On /\ B e. On ) -> ( A C_ B <-> ( A e. B \/ A = B ) ) )

Proof

Step Hyp Ref Expression
1 eloni 
 |-  ( A e. On -> Ord A )
2 eloni 
 |-  ( B e. On -> Ord B )
3 ordsseleq 
 |-  ( ( Ord A /\ Ord B ) -> ( A C_ B <-> ( A e. B \/ A = B ) ) )
4 1 2 3 syl2an 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B <-> ( A e. B \/ A = B ) ) )