Definition df-sn 4626

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 4718. For an alternate definition see dfsn2 4638. (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 4625	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1533	. . . 4 class 𝑥
5	4, 1	wceq 1534	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2705	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1534	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  4635  elsng  4639  absn  4643  dfsn2ALT  4645  rabsssn  4667  csbsng  4709  pw0  4812  iunidOLD  5059  uniabio  6510  iotaval  6514  dfimafn2  6957  fnsnfvOLD  6973  suppvalbr  8164  snec  8793  fset0  8867  0map0sn0  8898  infmap2  10236  cf0  10269  cflecard  10271  brdom7disj  10549  brdom6disj  10550  vdwlem6  16949  hashbc0  16968  symgbas0  19337  pzriprnglem10  21410  pzriprnglem11  21411  psrbagsn  22001  ptcmplem2  23951  snclseqg  24014  nmoo0  30595  nmop0  31790  nmfn0  31791  disjabrex  32366  disjabrexf  32367  pstmfval  33492  hasheuni  33699  derang0  34774  dfiota3  35514  bj-nuliotaALT  36532  poimirlem28  37116  lineset  39206  abbi1sn  41702  frege54cor1c  43336  iotain  43845  csbsngVD  44323  dfaimafn2  46537  dfatsnafv2  46623  rnfdmpr  46652

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »