# Metamath Proof Explorer

## Theorem ss2ab

Description: Class abstractions in a subclass relationship. (Contributed by NM, 3-Jul-1994)

Ref Expression
Assertion ss2ab ${⊢}\left\{{x}|{\phi }\right\}\subseteq \left\{{x}|{\psi }\right\}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$

### Proof

Step Hyp Ref Expression
1 nfab1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\phi }\right\}$
2 nfab1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\psi }\right\}$
3 1 2 dfss2f ${⊢}\left\{{x}|{\phi }\right\}\subseteq \left\{{x}|{\psi }\right\}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left\{{x}|{\phi }\right\}\to {x}\in \left\{{x}|{\psi }\right\}\right)$
4 abid ${⊢}{x}\in \left\{{x}|{\phi }\right\}↔{\phi }$
5 abid ${⊢}{x}\in \left\{{x}|{\psi }\right\}↔{\psi }$
6 4 5 imbi12i ${⊢}\left({x}\in \left\{{x}|{\phi }\right\}\to {x}\in \left\{{x}|{\psi }\right\}\right)↔\left({\phi }\to {\psi }\right)$
7 6 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left\{{x}|{\phi }\right\}\to {x}\in \left\{{x}|{\psi }\right\}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$
8 3 7 bitri ${⊢}\left\{{x}|{\phi }\right\}\subseteq \left\{{x}|{\psi }\right\}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$