Theorem unisng

Description: A set equals the union of its singleton. Theorem 8.2 of Quine p. 53. (Contributed by NM, 13-Aug-2002)

	Ref	Expression
Assertion	unisng	⊢ ( 𝐴 ∈ 𝑉 → ∪ { 𝐴 } = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dfsn2	⊢ { 𝐴 } = { 𝐴 , 𝐴 }
2	1	unieqi	⊢ ∪ { 𝐴 } = ∪ { 𝐴 , 𝐴 }
3	2	a1i	⊢ ( 𝐴 ∈ 𝑉 → ∪ { 𝐴 } = ∪ { 𝐴 , 𝐴 } )
4		uniprg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ∪ { 𝐴 , 𝐴 } = ( 𝐴 ∪ 𝐴 ) )
5	4	anidms	⊢ ( 𝐴 ∈ 𝑉 → ∪ { 𝐴 , 𝐴 } = ( 𝐴 ∪ 𝐴 ) )
6		unidm	⊢ ( 𝐴 ∪ 𝐴 ) = 𝐴
7	6	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∪ 𝐴 ) = 𝐴 )
8	3 5 7	3eqtrd	⊢ ( 𝐴 ∈ 𝑉 → ∪ { 𝐴 } = 𝐴 )