Theorem dfsn2ALT

Description: Alternate definition of singleton, based on the (alternate) definition of pair. Definition 5.1 of TakeutiZaring p. 15. (Contributed by AV, 12-Jun-2022) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		oridm	$$⊢\left(x=A\vee x=A\right)\leftrightarrow x=A$$
2	1	abbii	$$⊢\left\{x|\left(x=A\vee x=A\right)\right\}=\left\{x|x=A\right\}$$
3		dfpr2	$$⊢\left\{A,A\right\}=\left\{x|\left(x=A\vee x=A\right)\right\}$$
4		df-sn	$$⊢\left\{A\right\}=\left\{x|x=A\right\}$$
5	2 3 4	3eqtr4ri	$$⊢\left\{A\right\}=\left\{A,A\right\}$$