Definition df-sn 4586

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 4677. For an alternate definition see dfsn2 4598. (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 4585	. 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  4595  elsng  4599  absn  4605  dfsn2ALT  4607  rabsssn  4628  csbsng  4668  pw0  4772  iunidOLD  5020  uniabio  6466  iotaval  6470  dfimafn2  6906  suppvalbr  8120  snec  8728  fset0  8804  0map0sn0  8835  infmap2  10146  cf0  10180  cflecard  10182  brdom7disj  10460  brdom6disj  10461  vdwlem6  16933  hashbc0  16952  symgbas0  19303  pzriprnglem10  21432  pzriprnglem11  21433  psrbagsn  22003  ptcmplem2  23973  snclseqg  24036  1p1e2s  28343  twocut  28350  halfcut  28381  nmoo0  30770  nmop0  31965  nmfn0  31966  disjabrex  32561  disjabrexf  32562  pstmfval  33879  hasheuni  34068  derang0  35149  dfiota3  35904  bj-nuliotaALT  37039  poimirlem28  37635  dmcnvep  38354  lineset  39725  abbi1sn  42204  absnw  42659  frege54cor1c  43897  iotain  44399  csbsngVD  44875  dfaimafn2  47160  dfatsnafv2  47246  rnfdmpr  47275  stgr1  47953