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 AVsucABAB

Proof

Step Hyp Ref Expression
1 sucidg AVAsucA
2 ssel sucABAsucAAB
3 1 2 syl5com AVsucABAB