Definition df-sn 4583

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 4676. For an alternate definition see dfsn2 4595. (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 4582	. 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  4592  elsng  4596  absn  4602  dfsn2ALT  4604  rabsssn  4627  csbsng  4667  pw0  4770  moabex  5415  uniabio  6472  iotaval  6476  dfimafn2  6907  suppvalbr  8118  snecg  8728  snec  8729  fset0  8805  0map0sn0  8837  infmap2  10141  cf0  10175  cflecard  10177  brdom7disj  10455  brdom6disj  10456  vdwlem6  16928  hashbc0  16947  symgbas0  19335  pzriprnglem10  21462  pzriprnglem11  21463  psrbagsn  22035  ptcmplem2  24014  snclseqg  24077  twocut  28436  halfcut  28471  pw2cut2  28475  nmoo0  30885  nmop0  32080  nmfn0  32081  disjabrex  32675  disjabrexf  32676  pstmfval  34080  hasheuni  34269  derang0  35391  dfiota3  36143  bj-nuliotaALT  37333  poimirlem28  37928  dmcnvep  38668  ecqmap  38729  lineset  40143  abbi1sn  42624  absnw  43065  frege54cor1c  44300  iotain  44802  csbsngVD  45277  dfaimafn2  47555  dfatsnafv2  47641  rnfdmpr  47670  stgr1  48350