MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sn Structured version   Visualization version   GIF version

Definition df-sn 4371
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 4444. For an alternate definition see dfsn2 4383. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
df-sn {𝐴} = {𝑥𝑥 = 𝐴}
Distinct variable group:   𝑥,𝐴

Detailed syntax breakdown of Definition df-sn
StepHypRef Expression
1 cA . . 3 class 𝐴
21csn 4370 . 2 class {𝐴}
3 vx . . . . 5 setvar 𝑥
43cv 1636 . . . 4 class 𝑥
54, 1wceq 1637 . . 3 wff 𝑥 = 𝐴
65, 3cab 2792 . 2 class {𝑥𝑥 = 𝐴}
72, 6wceq 1637 1 wff {𝐴} = {𝑥𝑥 = 𝐴}
Colors of variables: wff setvar class
This definition is referenced by:  sneq  4380  elsng  4384  absn  4388  dfsn2ALT  4390  rabsssn  4408  csbsng  4435  pw0  4533  iunid  4767  uniabio  6070  dfimafn2  6463  fnsnfv  6475  suppvalbr  7529  snec  8041  infmap2  9321  cf0  9354  cflecard  9356  brdom7disj  9634  brdom6disj  9635  vdwlem6  15903  hashbc0  15922  symgbas0  18011  psrbagsn  19699  ptcmplem2  22066  snclseqg  22128  nmoo0  27970  nmop0  29169  nmfn0  29170  disjabrex  29716  disjabrexf  29717  pstmfval  30260  hasheuni  30468  derang0  31469  dfiota3  32346  bj-nuliotaALT  33325  poimirlem28  33745  lineset  35513  frege54cor1c  38703  iotain  39111  csbsngVD  39617  dfaimafn2  41749  dfatsnafv2  41835  rnfdmpr  41865
  Copyright terms: Public domain W3C validator