Definition df-sn 4569

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 4662. For an alternate definition see dfsn2 4581. (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 4568	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1541	. . . 4 class 𝑥
5	4, 1	wceq 1542	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2715	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1542	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  4578  elsng  4582  absn  4588  dfsn2ALT  4590  rabsssn  4613  csbsng  4653  pw0  4756  moabex  5409  uniabio  6466  iotaval  6470  dfimafn2  6901  suppvalbr  8111  snecg  8721  snec  8722  fset0  8798  0map0sn0  8830  infmap2  10136  cf0  10170  cflecard  10172  brdom7disj  10450  brdom6disj  10451  vdwlem6  16954  hashbc0  16973  symgbas0  19361  pzriprnglem10  21467  pzriprnglem11  21468  psrbagsn  22038  ptcmplem2  24015  snclseqg  24078  twocut  28412  halfcut  28447  pw2cut2  28451  nmoo0  30859  nmop0  32054  nmfn0  32055  disjabrex  32649  disjabrexf  32650  pstmfval  34037  hasheuni  34226  derang0  35348  dfiota3  36100  bj-nuliotaALT  37362  poimirlem28  37966  dmcnvep  38706  ecqmap  38767  lineset  40181  abbi1sn  42661  absnw  43108  frege54cor1c  44339  iotain  44841  csbsngVD  45316  dfaimafn2  47605  dfatsnafv2  47691  rnfdmpr  47720  stgr1  48428