Metamath Proof Explorer


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
|- A e. _V
Assertion intid
|- |^| { x | A e. x } = { A }

Proof

Step Hyp Ref Expression
1 intid.1
 |-  A e. _V
2 snex
 |-  { A } e. _V
3 eleq2
 |-  ( x = { A } -> ( A e. x <-> A e. { A } ) )
4 1 snid
 |-  A e. { A }
5 3 4 intmin3
 |-  ( { A } e. _V -> |^| { x | A e. x } C_ { A } )
6 2 5 ax-mp
 |-  |^| { x | A e. x } C_ { A }
7 1 elintab
 |-  ( A e. |^| { x | A e. x } <-> A. x ( A e. x -> A e. x ) )
8 id
 |-  ( A e. x -> A e. x )
9 7 8 mpgbir
 |-  A e. |^| { x | A e. x }
10 snssi
 |-  ( A e. |^| { x | A e. x } -> { A } C_ |^| { x | A e. x } )
11 9 10 ax-mp
 |-  { A } C_ |^| { x | A e. x }
12 6 11 eqssi
 |-  |^| { x | A e. x } = { A }