Theorem dfsn2ALT

Description: Alternate definition of singleton, based on the (alternate) definition of unordered 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	⊢ { 𝐴 } = { 𝐴 , 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		oridm	⊢ ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐴 ) ↔ 𝑥 = 𝐴 )
2	1	abbii	⊢ { 𝑥 ∣ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐴 ) } = { 𝑥 ∣ 𝑥 = 𝐴 }
3		dfpr2	⊢ { 𝐴 , 𝐴 } = { 𝑥 ∣ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐴 ) }
4		df-sn	⊢ { 𝐴 } = { 𝑥 ∣ 𝑥 = 𝐴 }
5	2 3 4	3eqtr4ri	⊢ { 𝐴 } = { 𝐴 , 𝐴 }