Definition df-sn 4589

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 4588	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1569	. . . 4 class 𝑥
5	4, 1	wceq 1570	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2741	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1570	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is used by:  sneq  4594  elsng  4598  absn  4604  dfsn2ALT  4606  rabsssn  4629  csbsng  4669  pw0  4833  moabex  5430  uniabio  6523  iotaval  6527  iotain  6528  dfimafn2  6968  suppvalbr  8205  suppvalbrOLD  8206  snecg  8823  snec  8824  fset0  8901  0map0sn0  8938  infmap2  10319  cf0  10352  cflecard  10354  brdom7disj  10634  brdom6disj  10635  vdwlem6  17190  hashbc0  17209  symgbas0  19630  pzriprnglem10  21823  pzriprnglem11  21824  psrbagsn  22399  ptcmplem2  24399  snclseqg  24462  twocut  28836  halfcut  28871  pw2cut2  28875  nmoo0  31420  nmop0  32615  nmfn0  32616  disjabrex  33245  disjabrexf  33246  pstmfval  34595  hasheuni  34784  derang0  36100  dfiota3  36862  bj-nuliotaALT  38163  poimirlem28  38757  dfproplem  38832  dmcnvep  39511  ecqmap  39572  lineset  40986  abbi1sn  43468  absnw  43880  frege54cor1c  45105  csbsngVD  46064  dfaimafn2  48439  dfatsnafv2  48525  rnfdmpr  48554  stgr1  49262