Definition df-sn 4568

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 4653. For an alternate definition see dfsn2 4580. (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 4567	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1536	. . . 4 class 𝑥
5	4, 1	wceq 1537	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2799	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1537	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  4577  elsng  4581  absn  4585  dfsn2ALT  4587  rabsssn  4607  csbsng  4644  pw0  4745  iunid  4984  uniabio  6328  dfimafn2  6729  fnsnfv  6743  suppvalbr  7834  snec  8360  0map0sn0  8449  infmap2  9640  cf0  9673  cflecard  9675  brdom7disj  9953  brdom6disj  9954  vdwlem6  16322  hashbc0  16341  symgbas0  18517  psrbagsn  20275  ptcmplem2  22661  snclseqg  22724  nmoo0  28568  nmop0  29763  nmfn0  29764  disjabrex  30332  disjabrexf  30333  pstmfval  31136  hasheuni  31344  derang0  32416  dfiota3  33384  bj-nuliotaALT  34354  poimirlem28  34935  lineset  36889  frege54cor1c  40310  iotain  40798  csbsngVD  41276  dfaimafn2  43414  dfatsnafv2  43500  rnfdmpr  43529