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	⊢ 𝐴 ∈ V
Assertion	intid	⊢ ∩ { 𝑥 ∣ 𝐴 ∈ 𝑥 } = { 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		intid.1	⊢ 𝐴 ∈ V
2		snex	⊢ { 𝐴 } ∈ V
3		eleq2	⊢ ( 𝑥 = { 𝐴 } → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ { 𝐴 } ) )
4	1	snid	⊢ 𝐴 ∈ { 𝐴 }
5	3 4	intmin3	⊢ ( { 𝐴 } ∈ V → ∩ { 𝑥 ∣ 𝐴 ∈ 𝑥 } ⊆ { 𝐴 } )
6	2 5	ax-mp	⊢ ∩ { 𝑥 ∣ 𝐴 ∈ 𝑥 } ⊆ { 𝐴 }
7	1	elintab	⊢ ( 𝐴 ∈ ∩ { 𝑥 ∣ 𝐴 ∈ 𝑥 } ↔ ∀ 𝑥 ( 𝐴 ∈ 𝑥 → 𝐴 ∈ 𝑥 ) )
8		id	⊢ ( 𝐴 ∈ 𝑥 → 𝐴 ∈ 𝑥 )
9	7 8	mpgbir	⊢ 𝐴 ∈ ∩ { 𝑥 ∣ 𝐴 ∈ 𝑥 }
10		snssi	⊢ ( 𝐴 ∈ ∩ { 𝑥 ∣ 𝐴 ∈ 𝑥 } → { 𝐴 } ⊆ ∩ { 𝑥 ∣ 𝐴 ∈ 𝑥 } )
11	9 10	ax-mp	⊢ { 𝐴 } ⊆ ∩ { 𝑥 ∣ 𝐴 ∈ 𝑥 }
12	6 11	eqssi	⊢ ∩ { 𝑥 ∣ 𝐴 ∈ 𝑥 } = { 𝐴 }