Theorem intmin2

Description: Any set is the smallest of all sets that include it. (Contributed by NM, 20-Sep-2003)

	Ref	Expression
Hypothesis	intmin2.1	$$⊢A\in \mathrm{V}$$
Assertion	intmin2	$$⊢\bigcap \left\{x|A\subseteq x\right\}=A$$

Proof

Step	Hyp	Ref	Expression
1		intmin2.1	$$⊢A\in \mathrm{V}$$
2		rabab	$$⊢\left\{x\in \mathrm{V}|A\subseteq x\right\}=\left\{x|A\subseteq x\right\}$$
3	2	inteqi	$$⊢\bigcap \left\{x\in \mathrm{V}|A\subseteq x\right\}=\bigcap \left\{x|A\subseteq x\right\}$$
4		intmin	$$⊢A\in \mathrm{V}\to \bigcap \left\{x\in \mathrm{V}|A\subseteq x\right\}=A$$
5	1 4	ax-mp	$$⊢\bigcap \left\{x\in \mathrm{V}|A\subseteq x\right\}=A$$
6	3 5	eqtr3i	$$⊢\bigcap \left\{x|A\subseteq x\right\}=A$$