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

Definition df-sn 3981
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 3993. (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 3980 . 2  class  { A }
3 vx . . . . 5  setvar  x
43cv 1454 . . . 4  class  x
54, 1wceq 1455 . . 3  wff  x  =  A
65, 3cab 2448 . 2  class  { x  |  x  =  A }
72, 6wceq 1455 1  wff  { A }  =  { x  |  x  =  A }
Colors of variables: wff setvar class
This definition is referenced by:  sneq  3990  elsn  3994  elsncg  4003  rabeqsn  4013  rabsssn  4014  csbsng  4042  rabsn  4052  pw0  4132  iunid  4347  dfiota2  5570  uniabio  5579  dfimafn2  5942  fnsnfv  5953  suppvalbr  6950  snec  7457  infmap2  8679  cf0  8712  cflecard  8714  brdom7disj  8990  brdom6disj  8991  vdwlem6  14991  hashbc0  15012  symgbas0  17090  psrbagsn  18773  ptcmplem2  21123  snclseqg  21185  nmoo0  26488  nmop0  27695  nmfn0  27696  disjabrex  28246  disjabrexf  28247  pstmfval  28750  hasheuni  28957  derang0  29942  dfiota3  30740  bj-nuliotaALT  31670  poimirlem28  32014  lineset  33349  frege54cor1c  36557  iotain  36813  csbsngVD  37331  dfaimafn2  38803  rnfdmpr  39153
  Copyright terms: Public domain W3C validator