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\}\leftrightarrow \forall x\in B\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\}\leftrightarrow 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)\leftrightarrow \left(x\in B\to \left(\phi \to A\subseteq x\right)\right)$$
5	4	albii	$$⊢\forall x\left(\left(x\in B\wedge \phi \right)\to A\subseteq x\right)\leftrightarrow \forall x\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\}\leftrightarrow \forall x\left(\left(x\in B\wedge \phi \right)\to A\subseteq x\right)$$
7		df-ral	$$⊢\forall x\in B\left(\phi \to A\subseteq x\right)\leftrightarrow \forall x\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\}\leftrightarrow \forall x\in B\left(\phi \to A\subseteq x\right)$$
9	3 8	bitri	$$⊢A\subseteq \bigcap \left\{x\in B|\phi \right\}\leftrightarrow \forall x\in B\left(\phi \to A\subseteq x\right)$$