Definition df-sn 4588

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 4681. For an alternate definition see dfsn2 4600. (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 4587	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1569	. . . 4 class 𝑥
5	4, 1	wceq 1570	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2740	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1570	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is used by:  sneq  4597  elsng  4601  absn  4607  dfsn2ALT  4609  rabsssn  4632  csbsng  4672  pw0  4776  moabex  5437  uniabio  6507  iotaval  6511  dfimafn2  6945  suppvalbr  8165  snecg  8780  snec  8781  fset0  8858  0map0sn0  8895  infmap2  10222  cf0  10255  cflecard  10257  brdom7disj  10537  brdom6disj  10538  vdwlem6  17082  hashbc0  17101  symgbas0  19517  pzriprnglem10  21704  pzriprnglem11  21705  psrbagsn  22280  ptcmplem2  24280  snclseqg  24343  twocut  28686  halfcut  28721  pw2cut2  28725  nmoo0  31258  nmop0  32453  nmfn0  32454  disjabrex  33042  disjabrexf  33043  pstmfval  34393  hasheuni  34582  derang0  35735  dfiota3  36487  bj-nuliotaALT  37789  poimirlem28  38384  dmcnvep  39123  ecqmap  39184  lineset  40598  abbi1sn  43080  absnw  43511  frege54cor1c  44742  iotain  45228  csbsngVD  45702  dfaimafn2  48041  dfatsnafv2  48127  rnfdmpr  48156  stgr1  48864