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 V x | A x = A

Proof

Step Hyp Ref Expression
1 snexg A V A V
2 snidg A V A A
3 eleq2 x = A A x A A
4 1 2 3 elabd A V A x | A x
5 intss1 A x | A x x | A x A
6 4 5 syl A V x | A x A
7 id A x A x
8 7 ax-gen x A x A x
9 elintabg A V A x | A x x A x A x
10 8 9 mpbiri A V A x | A x
11 10 snssd A V A x | A x
12 6 11 eqssd A V x | A x = A