Definition df-sn 4526

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 4613. For an alternate definition see dfsn2 4538. (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 4525	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1537	. . . 4 class 𝑥
5	4, 1	wceq 1538	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2776	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1538	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  4535  elsng  4539  absn  4543  dfsn2ALT  4545  rabsssn  4567  csbsng  4604  pw0  4705  iunid  4947  uniabio  6297  dfimafn2  6704  fnsnfv  6718  suppvalbr  7817  snec  8343  0map0sn0  8432  infmap2  9629  cf0  9662  cflecard  9664  brdom7disj  9942  brdom6disj  9943  vdwlem6  16312  hashbc0  16331  symgbas0  18509  psrbagsn  20734  ptcmplem2  22658  snclseqg  22721  nmoo0  28574  nmop0  29769  nmfn0  29770  disjabrex  30345  disjabrexf  30346  pstmfval  31249  hasheuni  31454  derang0  32529  dfiota3  33497  bj-nuliotaALT  34475  poimirlem28  35085  lineset  37034  frege54cor1c  40616  iotain  41121  csbsngVD  41599  dfaimafn2  43722  dfatsnafv2  43808  rnfdmpr  43837