Theorem ssmin

Description: Subclass of the minimum value of class of supersets. (Contributed by NM, 10-Aug-2006)

	Ref	Expression
Assertion	ssmin	$$⊢A\subseteq \bigcap \left\{x|\left(A\subseteq x\wedge \phi \right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ssintab	$$⊢A\subseteq \bigcap \left\{x|\left(A\subseteq x\wedge \phi \right)\right\}\leftrightarrow \forall x\left(\left(A\subseteq x\wedge \phi \right)\to A\subseteq x\right)$$
2		simpl	$$⊢\left(A\subseteq x\wedge \phi \right)\to A\subseteq x$$
3	1 2	mpgbir	$$⊢A\subseteq \bigcap \left\{x|\left(A\subseteq x\wedge \phi \right)\right\}$$