Metamath Proof Explorer

Theorem onsssuc

Description: A subset of an ordinal number belongs to its successor. (Contributed by NM, 15-Sep-1995)

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

Proof

Step Hyp Ref Expression
1 eloni 
 |-  ( B e. On -> Ord B )
2 ordsssuc 
 |-  ( ( A e. On /\ Ord B ) -> ( A C_ B <-> A e. suc B ) )
3 1 2 sylan2 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B <-> A e. suc B ) )