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 4565
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 4652. For an alternate definition see dfsn2 4577. (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 4564 . 2 class {𝐴}
3 vx . . . . 5 setvar 𝑥
43cv 1529 . . . 4 class 𝑥
54, 1wceq 1530 . . 3 wff 𝑥 = 𝐴
65, 3cab 2804 . 2 class {𝑥𝑥 = 𝐴}
72, 6wceq 1530 1 wff {𝐴} = {𝑥𝑥 = 𝐴}
Colors of variables: wff setvar class
This definition is referenced by:  sneq  4574  elsng  4578  absn  4582  dfsn2ALT  4584  rabsssn  4604  csbsng  4643  pw0  4744  iunid  4981  uniabio  6327  dfimafn2  6728  fnsnfv  6742  suppvalbr  7830  snec  8355  infmap2  9634  cf0  9667  cflecard  9669  brdom7disj  9947  brdom6disj  9948  vdwlem6  16317  hashbc0  16336  symgbas0  18458  psrbagsn  20210  ptcmplem2  22596  snclseqg  22658  nmoo0  28501  nmop0  29696  nmfn0  29697  disjabrex  30266  disjabrexf  30267  pstmfval  31041  hasheuni  31249  derang0  32319  dfiota3  33287  bj-nuliotaALT  34251  poimirlem28  34806  lineset  36760  frege54cor1c  40145  iotain  40633  csbsngVD  41111  dfaimafn2  43250  dfatsnafv2  43336  rnfdmpr  43365  efmndbas0  43962
  Copyright terms: Public domain W3C validator