Definition df-sn 4578

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

This definition is referenced by:  sneq  4587  elsng  4591  absn  4597  dfsn2ALT  4599  rabsssn  4620  csbsng  4660  pw0  4763  iunidOLD  5010  uniabio  6452  iotaval  6456  dfimafn2  6886  suppvalbr  8097  snec  8705  fset0  8781  0map0sn0  8812  infmap2  10111  cf0  10145  cflecard  10147  brdom7disj  10425  brdom6disj  10426  vdwlem6  16898  hashbc0  16917  symgbas0  19268  pzriprnglem10  21397  pzriprnglem11  21398  psrbagsn  21968  ptcmplem2  23938  snclseqg  24001  1p1e2s  28308  twocut  28315  halfcut  28346  nmoo0  30735  nmop0  31930  nmfn0  31931  disjabrex  32526  disjabrexf  32527  pstmfval  33869  hasheuni  34058  derang0  35152  dfiota3  35907  bj-nuliotaALT  37042  poimirlem28  37638  dmcnvep  38357  lineset  39727  abbi1sn  42206  absnw  42661  frege54cor1c  43898  iotain  44400  csbsngVD  44876  dfaimafn2  47160  dfatsnafv2  47246  rnfdmpr  47275  stgr1  47955