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	⊢ 𝐴 ∈ V
Assertion	intsn	⊢ ∩ { 𝐴 } = 𝐴

Proof

Step	Hyp	Ref	Expression
1		intsn.1	⊢ 𝐴 ∈ V
2		intsng	⊢ ( 𝐴 ∈ V → ∩ { 𝐴 } = 𝐴 )
3	1 2	ax-mp	⊢ ∩ { 𝐴 } = 𝐴