Definition df-sn 4586

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 4677. For an alternate definition see dfsn2 4598. (Contributed by NM, 21-Jun-1993.)

Assertion

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

Distinct variable group:   𝑥,𝐴

Detailed syntax breakdown of Definition df-sn

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	csn 4585	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1539	. . . 4 class 𝑥
5	4, 1	wceq 1540	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2707	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1540	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  4595  elsng  4599  absn  4605  dfsn2ALT  4607  rabsssn  4628  csbsng  4668  pw0  4772  iunidOLD  5020  uniabio  6466  iotaval  6470  dfimafn2  6906  suppvalbr  8120  snec  8728  fset0  8804  0map0sn0  8835  infmap2  10146  cf0  10180  cflecard  10182  brdom7disj  10460  brdom6disj  10461  vdwlem6  16933  hashbc0  16952  symgbas0  19295  pzriprnglem10  21376  pzriprnglem11  21377  psrbagsn  21946  ptcmplem2  23916  snclseqg  23979  1p1e2s  28278  twocut  28285  halfcut  28309  nmoo0  30693  nmop0  31888  nmfn0  31889  disjabrex  32484  disjabrexf  32485  pstmfval  33859  hasheuni  34048  derang0  35129  dfiota3  35884  bj-nuliotaALT  37019  poimirlem28  37615  dmcnvep  38334  lineset  39705  abbi1sn  42184  absnw  42639  frege54cor1c  43877  iotain  44379  csbsngVD  44855  dfaimafn2  47140  dfatsnafv2  47226  rnfdmpr  47255  stgr1  47933