Definition df-sn 4584

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 4596. (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 4583	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1569	. . . 4 class 𝑥
5	4, 1	wceq 1570	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2738	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1570	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is used by:  sneq  4593  elsng  4597  absn  4603  dfsn2ALT  4605  rabsssn  4628  csbsng  4668  pw0  4772  moabex  5425  uniabio  6497  iotaval  6501  dfimafn2  6936  suppvalbr  8159  snecg  8776  snec  8777  fset0  8854  0map0sn0  8891  infmap2  10266  cf0  10299  cflecard  10301  brdom7disj  10581  brdom6disj  10582  vdwlem6  17125  hashbc0  17144  symgbas0  19564  pzriprnglem10  21757  pzriprnglem11  21758  psrbagsn  22333  ptcmplem2  24333  snclseqg  24396  twocut  28742  halfcut  28777  pw2cut2  28781  nmoo0  31326  nmop0  32521  nmfn0  32522  disjabrex  33109  disjabrexf  33110  pstmfval  34461  hasheuni  34650  derang0  35855  dfiota3  36607  bj-nuliotaALT  37893  poimirlem28  38486  dfproplem  38561  dmcnvep  39240  ecqmap  39301  lineset  40715  abbi1sn  43197  absnw  43628  frege54cor1c  44859  iotain  45345  csbsngVD  45819  dfaimafn2  48158  dfatsnafv2  48244  rnfdmpr  48273  stgr1  48981