Definition df-sn 4559

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 4650. For an alternate definition see dfsn2 4571. (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 4558	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1542	. . . 4 class 𝑥
5	4, 1	wceq 1543	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2716	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1543	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  4568  elsng  4572  absn  4576  dfsn2ALT  4578  rabsssn  4600  csbsng  4641  pw0  4742  iunid  4986  uniabio  6388  dfimafn2  6812  fnsnfvOLD  6827  suppvalbr  7949  snec  8504  fset0  8577  0map0sn0  8608  infmap2  9880  cf0  9913  cflecard  9915  brdom7disj  10193  brdom6disj  10194  vdwlem6  16590  hashbc0  16609  symgbas0  18886  psrbagsn  21156  ptcmplem2  23087  snclseqg  23150  nmoo0  29029  nmop0  30224  nmfn0  30225  disjabrex  30797  disjabrexf  30798  pstmfval  31723  hasheuni  31928  derang0  33006  dfiota3  34127  bj-nuliotaALT  35131  poimirlem28  35711  lineset  37658  frege54cor1c  41385  iotain  41897  csbsngVD  42375  dfaimafn2  44518  dfatsnafv2  44604  rnfdmpr  44633