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 e. V -> |^| { x | A e. x } = { A } )

Proof

Step Hyp Ref Expression
1 snexg 
 |-  ( A e. V -> { A } e. _V )
2 snidg 
 |-  ( A e. V -> A e. { A } )
3 eleq2 
 |-  ( x = { A } -> ( A e. x <-> A e. { A } ) )
4 1 2 3 elabd 
 |-  ( A e. V -> { A } e. { x | A e. x } )
5 intss1 
 |-  ( { A } e. { x | A e. x } -> |^| { x | A e. x } C_ { A } )
6 4 5 syl 
 |-  ( A e. V -> |^| { x | A e. x } C_ { A } )
7 id 
 |-  ( A e. x -> A e. x )
8 7 ax-gen 
 |-  A. x ( A e. x -> A e. x )
9 elintabg 
 |-  ( A e. V -> ( A e. |^| { x | A e. x } <-> A. x ( A e. x -> A e. x ) ) )
10 8 9 mpbiri 
 |-  ( A e. V -> A e. |^| { x | A e. x } )
11 10 snssd 
 |-  ( A e. V -> { A } C_ |^| { x | A e. x } )
12 6 11 eqssd 
 |-  ( A e. V -> |^| { x | A e. x } = { A } )