# Metamath Proof Explorer

## Theorem ssint

Description: Subclass of a class intersection. Theorem 5.11(viii) of Monk1 p. 52 and its converse. (Contributed by NM, 14-Oct-1999)

Ref Expression
Assertion ssint ${⊢}{A}\subseteq \bigcap {B}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{A}\subseteq {x}$

### Proof

Step Hyp Ref Expression
1 dfss3 ${⊢}{A}\subseteq \bigcap {B}↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in \bigcap {B}$
2 vex ${⊢}{y}\in \mathrm{V}$
3 2 elint2 ${⊢}{y}\in \bigcap {B}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{y}\in {x}$
4 3 ralbii ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in \bigcap {B}↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{y}\in {x}$
5 ralcom ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{y}\in {x}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {x}$
6 dfss3 ${⊢}{A}\subseteq {x}↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {x}$
7 6 ralbii ${⊢}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{A}\subseteq {x}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {x}$
8 5 7 bitr4i ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{y}\in {x}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{A}\subseteq {x}$
9 1 4 8 3bitri ${⊢}{A}\subseteq \bigcap {B}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{A}\subseteq {x}$