Theorem intsng

Description: Intersection of a singleton. (Contributed by Stefan O'Rear, 22-Feb-2015)

	Ref	Expression
Assertion	intsng	|- ( A e. V -> |^| { A } = A )

Proof

Step	Hyp	Ref	Expression
1		dfsn2	|- { A } = { A , A }
2	1	inteqi	|- |^| { A } = |^| { A , A }
3		intprg	|- ( ( A e. V /\ A e. V ) -> |^| { A , A } = ( A i^i A ) )
4	3	anidms	|- ( A e. V -> |^| { A , A } = ( A i^i A ) )
5		inidm	|- ( A i^i A ) = A
6	4 5	eqtrdi	|- ( A e. V -> |^| { A , A } = A )
7	2 6	eqtrid	|- ( A e. V -> |^| { A } = A )