Definition df-sn 4630

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 4722. For an alternate definition see dfsn2 4642. (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 4629	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1541	. . . 4 class 𝑥
5	4, 1	wceq 1542	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2710	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1542	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  4639  elsng  4643  absn  4647  dfsn2ALT  4649  rabsssn  4671  csbsng  4713  pw0  4816  iunidOLD  5065  uniabio  6511  iotaval  6515  dfimafn2  6956  fnsnfvOLD  6972  suppvalbr  8150  snec  8774  fset0  8848  0map0sn0  8879  infmap2  10213  cf0  10246  cflecard  10248  brdom7disj  10526  brdom6disj  10527  vdwlem6  16919  hashbc0  16938  symgbas0  19256  psrbagsn  21624  ptcmplem2  23557  snclseqg  23620  nmoo0  30044  nmop0  31239  nmfn0  31240  disjabrex  31813  disjabrexf  31814  pstmfval  32876  hasheuni  33083  derang0  34160  dfiota3  34895  bj-nuliotaALT  35939  poimirlem28  36516  lineset  38609  abbi1sn  41040  frege54cor1c  42666  iotain  43176  csbsngVD  43654  dfaimafn2  45874  dfatsnafv2  45960  rnfdmpr  45989  pzriprnglem10  46814  pzriprnglem11  46815