Theorem intsn

Description: The intersection of a singleton is its member. Theorem 70 of Suppes p. 41. (Contributed by NM, 29-Sep-2002)

	Ref	Expression
Hypothesis	intsn.1	|- A e. _V
Assertion	intsn	|- |^| { A } = A

Proof

Step	Hyp	Ref	Expression
1		intsn.1	|- A e. _V
2		intsng	|- ( A e. _V -> |^| { A } = A )
3	1 2	ax-mp	|- |^| { A } = A