Theorem ssintab

Description: Subclass of the intersection of a class abstraction. (Contributed by NM, 31-Jul-2006) (Proof shortened by Andrew Salmon, 9-Jul-2011)

	Ref	Expression
Assertion	ssintab	$$⊢A\subseteq \bigcap \left\{x|\phi \right\}\leftrightarrow \forall x\left(\phi \to A\subseteq x\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssint	$$⊢A\subseteq \bigcap \left\{x|\phi \right\}\leftrightarrow \forall y\in \left\{x|\phi \right\}A\subseteq y$$
2		sseq2	$$⊢y=x\to \left(A\subseteq y\leftrightarrow A\subseteq x\right)$$
3	2	ralab2	$$⊢\forall y\in \left\{x|\phi \right\}A\subseteq y\leftrightarrow \forall x\left(\phi \to A\subseteq x\right)$$
4	1 3	bitri	$$⊢A\subseteq \bigcap \left\{x|\phi \right\}\leftrightarrow \forall x\left(\phi \to A\subseteq x\right)$$