# Metamath Proof Explorer

## Theorem ssrab

Description: Subclass of a restricted class abstraction. (Contributed by NM, 16-Aug-2006)

Ref Expression
Assertion ssrab ${⊢}{B}\subseteq \left\{{x}\in {A}|{\phi }\right\}↔\left({B}\subseteq {A}\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$

### Proof

Step Hyp Ref Expression
1 df-rab ${⊢}\left\{{x}\in {A}|{\phi }\right\}=\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}$
2 1 sseq2i ${⊢}{B}\subseteq \left\{{x}\in {A}|{\phi }\right\}↔{B}\subseteq \left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}$
3 ssab ${⊢}{B}\subseteq \left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to \left({x}\in {A}\wedge {\phi }\right)\right)$
4 dfss3 ${⊢}{B}\subseteq {A}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
5 4 anbi1i ${⊢}\left({B}\subseteq {A}\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{x}\in {A}\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
6 r19.26 ${⊢}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)↔\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{x}\in {A}\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
7 df-ral ${⊢}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to \left({x}\in {A}\wedge {\phi }\right)\right)$
8 5 6 7 3bitr2ri ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to \left({x}\in {A}\wedge {\phi }\right)\right)↔\left({B}\subseteq {A}\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
9 2 3 8 3bitri ${⊢}{B}\subseteq \left\{{x}\in {A}|{\phi }\right\}↔\left({B}\subseteq {A}\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$