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 }