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	|- { A } = { A , A }

Proof

Step	Hyp	Ref	Expression
1		oridm	|- ( ( x = A \/ x = A ) <-> x = A )
2	1	abbii	|- { x | ( x = A \/ x = A ) } = { x | x = A }
3		dfpr2	|- { A , A } = { x | ( x = A \/ x = A ) }
4		df-sn	|- { A } = { x | x = A }
5	2 3 4	3eqtr4ri	|- { A } = { A , A }