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 ) )