This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-sn

Description: Define the singleton of a class. Definition 7.1 of Quine p. 48. For convenience, it is well-defined for proper classes, i.e., those that are not elements of _V , see snprc . For an alternate definition see dfsn2 . (Contributed by NM, 21-Jun-1993)

		Ref	Expression
	Assertion	df-sn	⊢ { 𝐴 } = { 𝑥 ∣ 𝑥 = 𝐴 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	csn	⊢ { 𝐴 }
2		vx	⊢ 𝑥
3	2	cv	⊢ 𝑥
4	3 0	wceq	⊢ 𝑥 = 𝐴
5	4 2	cab	⊢ { 𝑥 ∣ 𝑥 = 𝐴 }
6	1 5	wceq	⊢ { 𝐴 } = { 𝑥 ∣ 𝑥 = 𝐴 }