Theorem intidg

Description: The intersection of all sets to which a set belongs is the singleton of that set. (Contributed by NM, 5-Jun-2009) Put in closed form and avoid ax-nul . (Revised by BJ, 17-Jan-2025)

	Ref	Expression
Assertion	intidg	$$⊢A\in V\to \bigcap \left\{x|A\in x\right\}=\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		snexg	$$⊢A\in V\to \left\{A\right\}\in \mathrm{V}$$
2		snidg	$$⊢A\in V\to A\in \left\{A\right\}$$
3		eleq2	$$⊢x=\left\{A\right\}\to \left(A\in x\leftrightarrow A\in \left\{A\right\}\right)$$
4	1 2 3	elabd	$$⊢A\in V\to \left\{A\right\}\in \left\{x|A\in x\right\}$$
5		intss1	$$⊢\left\{A\right\}\in \left\{x|A\in x\right\}\to \bigcap \left\{x|A\in x\right\}\subseteq \left\{A\right\}$$
6	4 5	syl	$$⊢A\in V\to \bigcap \left\{x|A\in x\right\}\subseteq \left\{A\right\}$$
7		id	$$⊢A\in x\to A\in x$$
8	7	ax-gen	$$⊢\forall x\left(A\in x\to A\in x\right)$$
9		elintabg	$$⊢A\in V\to \left(A\in \bigcap \left\{x|A\in x\right\}\leftrightarrow \forall x\left(A\in x\to A\in x\right)\right)$$
10	8 9	mpbiri	$$⊢A\in V\to A\in \bigcap \left\{x|A\in x\right\}$$
11	10	snssd	$$⊢A\in V\to \left\{A\right\}\subseteq \bigcap \left\{x|A\in x\right\}$$
12	6 11	eqssd	$$⊢A\in V\to \bigcap \left\{x|A\in x\right\}=\left\{A\right\}$$