Definition df-sn 4649

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 4742. For an alternate definition see dfsn2 4661. (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 4648	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1536	. . . 4 class 𝑥
5	4, 1	wceq 1537	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2717	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1537	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  4658  elsng  4662  absn  4667  dfsn2ALT  4669  rabsssn  4690  csbsng  4733  pw0  4837  iunidOLD  5084  uniabio  6540  iotaval  6544  dfimafn2  6985  suppvalbr  8205  snec  8838  fset0  8912  0map0sn0  8943  infmap2  10286  cf0  10320  cflecard  10322  brdom7disj  10600  brdom6disj  10601  vdwlem6  17033  hashbc0  17052  symgbas0  19430  pzriprnglem10  21524  pzriprnglem11  21525  psrbagsn  22110  ptcmplem2  24082  snclseqg  24145  1p1e2s  28418  nohalf  28425  halfcut  28434  nmoo0  30823  nmop0  32018  nmfn0  32019  disjabrex  32604  disjabrexf  32605  pstmfval  33842  hasheuni  34049  derang0  35137  dfiota3  35887  bj-nuliotaALT  37024  poimirlem28  37608  lineset  39695  abbi1sn  42216  absnw  42633  frege54cor1c  43877  iotain  44386  csbsngVD  44864  dfaimafn2  47081  dfatsnafv2  47167  rnfdmpr  47196