Definition df-sn 4126

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, although it is not very meaningful in this case. For an alternate definition see dfsn2 4138. (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 4125	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1474	. . . 4 class 𝑥
5	4, 1	wceq 1475	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2596	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1475	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  4135  elsng  4139  rabeqsn  4161  rabsssn  4162  csbsng  4190  rabsn  4200  pw0  4283  iunid  4511  dfiota2  5769  uniabio  5778  dfimafn2  6156  fnsnfv  6168  suppvalbr  7186  snec  7697  infmap2  8923  cf0  8956  cflecard  8958  brdom7disj  9234  brdom6disj  9235  vdwlem6  15528  hashbc0  15547  symgbas0  17637  psrbagsn  19316  ptcmplem2  21667  snclseqg  21729  nmoo0  27030  nmop0  28229  nmfn0  28230  disjabrex  28777  disjabrexf  28778  pstmfval  29267  hasheuni  29474  derang0  30405  dfiota3  31200  bj-nuliotaALT  32211  poimirlem28  32607  lineset  34042  frege54cor1c  37229  iotain  37640  csbsngVD  38151  dfaimafn2  39895  rnfdmpr  40325