Theorem dfsn2

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

	Ref	Expression
Assertion	dfsn2	$$⊢\left\{A\right\}=\left\{A,A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-pr	$$⊢\left\{A,A\right\}=\left\{A\right\}\cup \left\{A\right\}$$
2		unidm	$$⊢\left\{A\right\}\cup \left\{A\right\}=\left\{A\right\}$$
3	1 2	eqtr2i	$$⊢\left\{A\right\}=\left\{A,A\right\}$$