Metamath Proof Explorer

Theorem ssintrab

Description: Subclass of the intersection of a restricted class abstraction. (Contributed by NM, 30-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 df-rab ${⊢}\left\{{x}\in {B}|{\phi }\right\}=\left\{{x}|\left({x}\in {B}\wedge {\phi }\right)\right\}$
2 1 inteqi ${⊢}\bigcap \left\{{x}\in {B}|{\phi }\right\}=\bigcap \left\{{x}|\left({x}\in {B}\wedge {\phi }\right)\right\}$
3 2 sseq2i ${⊢}{A}\subseteq \bigcap \left\{{x}\in {B}|{\phi }\right\}↔{A}\subseteq \bigcap \left\{{x}|\left({x}\in {B}\wedge {\phi }\right)\right\}$
4 impexp ${⊢}\left(\left({x}\in {B}\wedge {\phi }\right)\to {A}\subseteq {x}\right)↔\left({x}\in {B}\to \left({\phi }\to {A}\subseteq {x}\right)\right)$
5 4 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {B}\wedge {\phi }\right)\to {A}\subseteq {x}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to \left({\phi }\to {A}\subseteq {x}\right)\right)$
6 ssintab ${⊢}{A}\subseteq \bigcap \left\{{x}|\left({x}\in {B}\wedge {\phi }\right)\right\}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {B}\wedge {\phi }\right)\to {A}\subseteq {x}\right)$
7 df-ral ${⊢}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {A}\subseteq {x}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to \left({\phi }\to {A}\subseteq {x}\right)\right)$
8 5 6 7 3bitr4i ${⊢}{A}\subseteq \bigcap \left\{{x}|\left({x}\in {B}\wedge {\phi }\right)\right\}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {A}\subseteq {x}\right)$
9 3 8 bitri ${⊢}{A}\subseteq \bigcap \left\{{x}\in {B}|{\phi }\right\}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {A}\subseteq {x}\right)$