Definition df-sn 4607

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 4697. For an alternate definition see dfsn2 4619. (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 4606	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1538	. . . 4 class 𝑥
5	4, 1	wceq 1539	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2712	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1539	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  4616  elsng  4620  absn  4625  dfsn2ALT  4627  rabsssn  4648  csbsng  4688  pw0  4792  iunidOLD  5041  uniabio  6507  iotaval  6511  dfimafn2  6951  suppvalbr  8170  snec  8801  fset0  8875  0map0sn0  8906  infmap2  10238  cf0  10272  cflecard  10274  brdom7disj  10552  brdom6disj  10553  vdwlem6  17005  hashbc0  17024  symgbas0  19373  pzriprnglem10  21462  pzriprnglem11  21463  psrbagsn  22034  ptcmplem2  24006  snclseqg  24069  1p1e2s  28335  nohalf  28342  halfcut  28351  nmoo0  30737  nmop0  31932  nmfn0  31933  disjabrex  32522  disjabrexf  32523  pstmfval  33829  hasheuni  34020  derang0  35108  dfiota3  35858  bj-nuliotaALT  36993  poimirlem28  37589  lineset  39674  abbi1sn  42196  absnw  42626  frege54cor1c  43866  iotain  44369  csbsngVD  44846  dfaimafn2  47112  dfatsnafv2  47198  rnfdmpr  47227  stgr1  47862