Theorem intid

Description: The intersection of all sets to which a set belongs is the singleton of that set. (Contributed by NM, 5-Jun-2009)

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

Proof

Step	Hyp	Ref	Expression
1		intid.1	$$⊢A\in \mathrm{V}$$
2		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
3		eleq2	$$⊢x=\left\{A\right\}\to \left(A\in x\leftrightarrow A\in \left\{A\right\}\right)$$
4	1	snid	$$⊢A\in \left\{A\right\}$$
5	3 4	intmin3	$$⊢\left\{A\right\}\in \mathrm{V}\to \bigcap \left\{x|A\in x\right\}\subseteq \left\{A\right\}$$
6	2 5	ax-mp	$$⊢\bigcap \left\{x|A\in x\right\}\subseteq \left\{A\right\}$$
7	1	elintab	$$⊢A\in \bigcap \left\{x|A\in x\right\}\leftrightarrow \forall x\left(A\in x\to A\in x\right)$$
8		id	$$⊢A\in x\to A\in x$$
9	7 8	mpgbir	$$⊢A\in \bigcap \left\{x|A\in x\right\}$$
10		snssi	$$⊢A\in \bigcap \left\{x|A\in x\right\}\to \left\{A\right\}\subseteq \bigcap \left\{x|A\in x\right\}$$
11	9 10	ax-mp	$$⊢\left\{A\right\}\subseteq \bigcap \left\{x|A\in x\right\}$$
12	6 11	eqssi	$$⊢\bigcap \left\{x|A\in x\right\}=\left\{A\right\}$$