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 V suc A B A B


Step Hyp Ref Expression
1 sucidg A V A suc A
2 ssel suc A B A suc A A B
3 1 2 syl5com A V suc A B A B