This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⋂ \{x \| A \in x\} = \{A\}$

Proof

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