Definition df-sn 4585

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 4678. For an alternate definition see dfsn2 4597. (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 4584	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1561	. . . 4 class 𝑥
5	4, 1	wceq 1562	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2742	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1562	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  4594  elsng  4598  absn  4604  dfsn2ALT  4606  rabsssn  4629  csbsng  4669  pw0  4772  moabex  5427  uniabio  6493  iotaval  6497  dfimafn2  6932  suppvalbr  8146  snecg  8761  snec  8762  fset0  8837  0map0sn0  8869  infmap2  10175  cf0  10209  cflecard  10211  brdom7disj  10490  brdom6disj  10491  vdwlem6  17024  hashbc0  17043  symgbas0  19431  pzriprnglem10  21544  pzriprnglem11  21545  psrbagsn  22118  ptcmplem2  24115  snclseqg  24178  twocut  28518  halfcut  28553  pw2cut2  28557  nmoo0  30996  nmop0  32191  nmfn0  32192  disjabrex  32784  disjabrexf  32785  pstmfval  34195  hasheuni  34384  derang0  35524  dfiota3  36276  bj-nuliotaALT  37548  poimirlem28  38152  dmcnvep  38892  ecqmap  38953  lineset  40367  abbi1sn  42847  absnw  43265  frege54cor1c  44496  iotain  44998  csbsngVD  45473  dfaimafn2  47765  dfatsnafv2  47851  rnfdmpr  47880  stgr1  48588