# Metamath Proof Explorer

## Theorem rabss

Description: Restricted class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006)

Ref Expression
Assertion rabss ${⊢}\left\{{x}\in {A}|{\phi }\right\}\subseteq {B}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}\in {B}\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 sseq1i ${⊢}\left\{{x}\in {A}|{\phi }\right\}\subseteq {B}↔\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}\subseteq {B}$
3 abss ${⊢}\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}\subseteq {B}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {\phi }\right)\to {x}\in {B}\right)$
4 impexp ${⊢}\left(\left({x}\in {A}\wedge {\phi }\right)\to {x}\in {B}\right)↔\left({x}\in {A}\to \left({\phi }\to {x}\in {B}\right)\right)$
5 4 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {\phi }\right)\to {x}\in {B}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({\phi }\to {x}\in {B}\right)\right)$
6 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}\in {B}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({\phi }\to {x}\in {B}\right)\right)$
7 5 6 bitr4i ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {\phi }\right)\to {x}\in {B}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}\in {B}\right)$
8 2 3 7 3bitri ${⊢}\left\{{x}\in {A}|{\phi }\right\}\subseteq {B}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}\in {B}\right)$