Theorem intsng

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

	Ref	Expression
Assertion	intsng	⊢ ( 𝐴 ∈ 𝑉 → ∩ { 𝐴 } = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dfsn2	⊢ { 𝐴 } = { 𝐴 , 𝐴 }
2	1	inteqi	⊢ ∩ { 𝐴 } = ∩ { 𝐴 , 𝐴 }
3		intprg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ∩ { 𝐴 , 𝐴 } = ( 𝐴 ∩ 𝐴 ) )
4	3	anidms	⊢ ( 𝐴 ∈ 𝑉 → ∩ { 𝐴 , 𝐴 } = ( 𝐴 ∩ 𝐴 ) )
5		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
6	4 5	eqtrdi	⊢ ( 𝐴 ∈ 𝑉 → ∩ { 𝐴 , 𝐴 } = 𝐴 )
7	2 6	eqtrid	⊢ ( 𝐴 ∈ 𝑉 → ∩ { 𝐴 } = 𝐴 )