**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 | $${\u22a2}{A}\in {V}\to \left(\mathrm{suc}{A}\subseteq {B}\to {A}\in {B}\right)$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | sucidg | $${\u22a2}{A}\in {V}\to {A}\in \mathrm{suc}{A}$$ | |

2 | ssel | $${\u22a2}\mathrm{suc}{A}\subseteq {B}\to \left({A}\in \mathrm{suc}{A}\to {A}\in {B}\right)$$ | |

3 | 1 2 | syl5com | $${\u22a2}{A}\in {V}\to \left(\mathrm{suc}{A}\subseteq {B}\to {A}\in {B}\right)$$ |