This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \in V$
	Assertion	intsn	$⊢ ⋂ \{A\} = A$

Step	Hyp	Ref	Expression
1		intsn.1	$⊢ A \in V$
2		intsng	$⊢ A \in V \to ⋂ \{A\} = A$
3	1 2	ax-mp	$⊢ ⋂ \{A\} = A$