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

Metamath Proof Explorer

Theorem intsng

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

		Ref	Expression
	Assertion	intsng	$⊢ A \in V \to ⋂ \{A\} = A$

Step	Hyp	Ref	Expression
1		dfsn2	$⊢ \{A\} = \{A, A\}$
2	1	inteqi	$⊢ ⋂ \{A\} = ⋂ \{A, A\}$
3		intprg	$⊢ (A \in V \land A \in V) \to ⋂ \{A, A\} = A \cap A$
4	3	anidms	$⊢ A \in V \to ⋂ \{A, A\} = A \cap A$
5		inidm	$⊢ A \cap A = A$
6	4 5	eqtrdi	$⊢ A \in V \to ⋂ \{A, A\} = A$
7	2 6	eqtrid	$⊢ A \in V \to ⋂ \{A\} = A$