Theorem dfsn2

Description: Alternate definition of singleton. Definition 5.1 of TakeutiZaring p. 15. (Contributed by NM, 24-Apr-1994)

	Ref	Expression
Assertion	dfsn2	⊢ { 𝐴 } = { 𝐴 , 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		df-pr	⊢ { 𝐴 , 𝐴 } = ( { 𝐴 } ∪ { 𝐴 } )
2		unidm	⊢ ( { 𝐴 } ∪ { 𝐴 } ) = { 𝐴 }
3	1 2	eqtr2i	⊢ { 𝐴 } = { 𝐴 , 𝐴 }