Theorem intmin

Description: Any member of a class is the smallest of those members that include it. (Contributed by NM, 13-Aug-2002) (Proof shortened by Andrew Salmon, 9-Jul-2011)

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

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢y\in \mathrm{V}$$
2	1	elintrab	$$⊢y\in \bigcap \left\{x\in B|A\subseteq x\right\}\leftrightarrow \forall x\in B\left(A\subseteq x\to y\in x\right)$$
3		ssid	$$⊢A\subseteq A$$
4		sseq2	$$⊢x=A\to \left(A\subseteq x\leftrightarrow A\subseteq A\right)$$
5		eleq2	$$⊢x=A\to \left(y\in x\leftrightarrow y\in A\right)$$
6	4 5	imbi12d	$$⊢x=A\to \left(\left(A\subseteq x\to y\in x\right)\leftrightarrow \left(A\subseteq A\to y\in A\right)\right)$$
7	6	rspcv	$$⊢A\in B\to \left(\forall x\in B\left(A\subseteq x\to y\in x\right)\to \left(A\subseteq A\to y\in A\right)\right)$$
8	3 7	mpii	$$⊢A\in B\to \left(\forall x\in B\left(A\subseteq x\to y\in x\right)\to y\in A\right)$$
9	2 8	biimtrid	$$⊢A\in B\to \left(y\in \bigcap \left\{x\in B|A\subseteq x\right\}\to y\in A\right)$$
10	9	ssrdv	$$⊢A\in B\to \bigcap \left\{x\in B|A\subseteq x\right\}\subseteq A$$
11		ssintub	$$⊢A\subseteq \bigcap \left\{x\in B|A\subseteq x\right\}$$
12	11	a1i	$$⊢A\in B\to A\subseteq \bigcap \left\{x\in B|A\subseteq x\right\}$$
13	10 12	eqssd	$$⊢A\in B\to \bigcap \left\{x\in B|A\subseteq x\right\}=A$$