Theorem ssintub

Description: Subclass of the least upper bound. (Contributed by NM, 8-Aug-2000)

	Ref	Expression
Assertion	ssintub	$$⊢A\subseteq \bigcap \left\{x\in B|A\subseteq x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ssint	$$⊢A\subseteq \bigcap \left\{x\in B|A\subseteq x\right\}\leftrightarrow \forall y\in \left\{x\in B|A\subseteq x\right\}A\subseteq y$$
2		sseq2	$$⊢x=y\to \left(A\subseteq x\leftrightarrow A\subseteq y\right)$$
3	2	elrab	$$⊢y\in \left\{x\in B|A\subseteq x\right\}\leftrightarrow \left(y\in B\wedge A\subseteq y\right)$$
4	3	simprbi	$$⊢y\in \left\{x\in B|A\subseteq x\right\}\to A\subseteq y$$
5	1 4	mprgbir	$$⊢A\subseteq \bigcap \left\{x\in B|A\subseteq x\right\}$$