Definition df-sn 4598

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 4689. For an alternate definition see dfsn2 4610. (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 4597	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1539	. . . 4 class 𝑥
5	4, 1	wceq 1540	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2708	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1540	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  4607  elsng  4611  absn  4617  dfsn2ALT  4619  rabsssn  4640  csbsng  4680  pw0  4784  iunidOLD  5033  uniabio  6486  iotaval  6490  dfimafn2  6931  suppvalbr  8152  snec  8757  fset0  8831  0map0sn0  8862  infmap2  10188  cf0  10222  cflecard  10224  brdom7disj  10502  brdom6disj  10503  vdwlem6  16963  hashbc0  16982  symgbas0  19325  pzriprnglem10  21406  pzriprnglem11  21407  psrbagsn  21976  ptcmplem2  23946  snclseqg  24009  1p1e2s  28309  twocut  28316  halfcut  28340  nmoo0  30727  nmop0  31922  nmfn0  31923  disjabrex  32518  disjabrexf  32519  pstmfval  33894  hasheuni  34083  derang0  35158  dfiota3  35908  bj-nuliotaALT  37043  poimirlem28  37639  lineset  39724  abbi1sn  42203  absnw  42638  frege54cor1c  43876  iotain  44378  csbsngVD  44854  dfaimafn2  47137  dfatsnafv2  47223  rnfdmpr  47252  stgr1  47915