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	⊢ ( 𝐴 ∈ 𝑉 → ∩ { 𝑥 ∣ 𝐴 ∈ 𝑥 } = { 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		snexg	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ∈ V )
2		snidg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
3		eleq2	⊢ ( 𝑥 = { 𝐴 } → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ { 𝐴 } ) )
4	1 2 3	elabd	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ∈ { 𝑥 ∣ 𝐴 ∈ 𝑥 } )
5		intss1	⊢ ( { 𝐴 } ∈ { 𝑥 ∣ 𝐴 ∈ 𝑥 } → ∩ { 𝑥 ∣ 𝐴 ∈ 𝑥 } ⊆ { 𝐴 } )
6	4 5	syl	⊢ ( 𝐴 ∈ 𝑉 → ∩ { 𝑥 ∣ 𝐴 ∈ 𝑥 } ⊆ { 𝐴 } )
7		id	⊢ ( 𝐴 ∈ 𝑥 → 𝐴 ∈ 𝑥 )
8	7	ax-gen	⊢ ∀ 𝑥 ( 𝐴 ∈ 𝑥 → 𝐴 ∈ 𝑥 )
9		elintabg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ∩ { 𝑥 ∣ 𝐴 ∈ 𝑥 } ↔ ∀ 𝑥 ( 𝐴 ∈ 𝑥 → 𝐴 ∈ 𝑥 ) ) )
10	8 9	mpbiri	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ ∩ { 𝑥 ∣ 𝐴 ∈ 𝑥 } )
11	10	snssd	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ⊆ ∩ { 𝑥 ∣ 𝐴 ∈ 𝑥 } )
12	6 11	eqssd	⊢ ( 𝐴 ∈ 𝑉 → ∩ { 𝑥 ∣ 𝐴 ∈ 𝑥 } = { 𝐴 } )