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

Definition df-sn 3945
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, although it is not very meaningful in this case. For an alternate definition see dfsn2 3957. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
df-sn  |-  { A }  =  { x  |  x  =  A }
Distinct variable group:    x, A

Detailed syntax breakdown of Definition df-sn
StepHypRef Expression
1 cA . . 3  class  A
21csn 3944 . 2  class  { A }
3 vx . . . . 5  setvar  x
43cv 1398 . . . 4  class  x
54, 1wceq 1399 . . 3  wff  x  =  A
65, 3cab 2367 . 2  class  { x  |  x  =  A }
72, 6wceq 1399 1  wff  { A }  =  { x  |  x  =  A }
Colors of variables: wff setvar class
This definition is referenced by:  sneq  3954  elsn  3958  elsncg  3967  csbsng  4002  rabsn  4011  pw0  4091  iunid  4298  dfiota2  5461  uniabio  5470  dfimafn2  5824  fnsnfv  5834  suppvalbr  6821  snec  7292  infmap2  8511  cf0  8544  cflecard  8546  brdom7disj  8822  brdom6disj  8823  vdwlem6  14506  hashbc0  14525  symgbas0  16536  psrbagsn  18273  ptcmplem2  20638  snclseqg  20699  nmoo0  25823  nmop0  27021  nmfn0  27022  disjabrex  27572  disjabrexf  27573  pstmfval  28029  hasheuni  28233  derang0  28802  dfiota3  29726  iotain  31492  dfaimafn2  32417  rnfdmpr  32629  rabeqsn  33119  rabsssn  33120  csbsngVD  34040  bj-nuliotaALT  34935  lineset  35875  frege54cor1c  38414
  Copyright terms: Public domain W3C validator