# Metamath Proof Explorer

## Theorem ssrabf

Description: Subclass of a restricted class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses ssrabf.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
ssrabf.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
Assertion ssrabf ${⊢}{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 ssrabf.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
2 ssrabf.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
3 df-rab ${⊢}\left\{{x}\in {A}|{\phi }\right\}=\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}$
4 3 sseq2i ${⊢}{B}\subseteq \left\{{x}\in {A}|{\phi }\right\}↔{B}\subseteq \left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}$
5 1 ssabf ${⊢}{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)$
6 1 2 dfss3f ${⊢}{B}\subseteq {A}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
7 6 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)$
8 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)$
9 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)$
10 7 8 9 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)$
11 4 5 10 3bitri ${⊢}{B}\subseteq \left\{{x}\in {A}|{\phi }\right\}↔\left({B}\subseteq {A}\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$