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 ( 𝐴𝑉 { 𝑥𝐴𝑥 } = { 𝐴 } )