Theorem intsng

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

	Ref	Expression
Assertion	intsng	$$⊢A\in V\to \bigcap \left\{A\right\}=A$$

Proof

Step	Hyp	Ref	Expression
1		dfsn2	$$⊢\left\{A\right\}=\left\{A,A\right\}$$
2	1	inteqi	$$⊢\bigcap \left\{A\right\}=\bigcap \left\{A,A\right\}$$
3		intprg	$$⊢\left(A\in V\wedge A\in V\right)\to \bigcap \left\{A,A\right\}=A\cap A$$
4	3	anidms	$$⊢A\in V\to \bigcap \left\{A,A\right\}=A\cap A$$
5		inidm	$$⊢A\cap A=A$$
6	4 5	eqtrdi	$$⊢A\in V\to \bigcap \left\{A,A\right\}=A$$
7	2 6	syl5eq	$$⊢A\in V\to \bigcap \left\{A\right\}=A$$