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 } )