# Metamath Proof Explorer

## Theorem ss2rab

Description: Restricted abstraction classes in a subclass relationship. (Contributed by NM, 30-May-1999)

Ref Expression
Assertion ss2rab ${⊢}\left\{{x}\in {A}|{\phi }\right\}\subseteq \left\{{x}\in {A}|{\psi }\right\}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\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 df-rab ${⊢}\left\{{x}\in {A}|{\psi }\right\}=\left\{{x}|\left({x}\in {A}\wedge {\psi }\right)\right\}$
3 1 2 sseq12i ${⊢}\left\{{x}\in {A}|{\phi }\right\}\subseteq \left\{{x}\in {A}|{\psi }\right\}↔\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}\subseteq \left\{{x}|\left({x}\in {A}\wedge {\psi }\right)\right\}$
4 ss2ab ${⊢}\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}\subseteq \left\{{x}|\left({x}\in {A}\wedge {\psi }\right)\right\}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {\phi }\right)\to \left({x}\in {A}\wedge {\psi }\right)\right)$
5 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({\phi }\to {\psi }\right)\right)$
6 imdistan ${⊢}\left({x}\in {A}\to \left({\phi }\to {\psi }\right)\right)↔\left(\left({x}\in {A}\wedge {\phi }\right)\to \left({x}\in {A}\wedge {\psi }\right)\right)$
7 6 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({\phi }\to {\psi }\right)\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {\phi }\right)\to \left({x}\in {A}\wedge {\psi }\right)\right)$
8 5 7 bitr2i ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {\phi }\right)\to \left({x}\in {A}\wedge {\psi }\right)\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$
9 3 4 8 3bitri ${⊢}\left\{{x}\in {A}|{\phi }\right\}\subseteq \left\{{x}\in {A}|{\psi }\right\}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$