Metamath Proof Explorer


Theorem sucssel

Description: A set whose successor is a subset of another class is a member of that class. (Contributed by NM, 16-Sep-1995)

Ref Expression
Assertion sucssel
|- ( A e. V -> ( suc A C_ B -> A e. B ) )

Proof

Step Hyp Ref Expression
1 sucidg
 |-  ( A e. V -> A e. suc A )
2 ssel
 |-  ( suc A C_ B -> ( A e. suc A -> A e. B ) )
3 1 2 syl5com
 |-  ( A e. V -> ( suc A C_ B -> A e. B ) )