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

Definition df-sn 3812
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 3820. (Contributed by NM, 5-Aug-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 3806 . 2  class  { A }
3 vx . . . . 5  set  x
43cv 1651 . . . 4  class  x
54, 1wceq 1652 . . 3  wff  x  =  A
65, 3cab 2421 . 2  class  { x  |  x  =  A }
72, 6wceq 1652 1  wff  { A }  =  { x  |  x  =  A }
Colors of variables: wff set class
This definition is referenced by:  sneq  3817  elsn  3821  elsncg  3828  csbsng  3859  rabsn  3865  pw0  3937  iunid  4138  dfiota2  5411  uniabio  5420  dfimafn2  5768  fnsnfv  5778  snec  6959  infmap2  8090  cf0  8123  cflecard  8125  brdom7disj  8401  brdom6disj  8402  vdwlem6  13346  hashbc0  13365  psrbagsn  16547  ptcmplem2  18076  snclseqg  18137  nmoo0  22284  nmop0  23481  nmfn0  23482  disjabrex  24016  disjabrexf  24017  pstmfval  24283  hasheuni  24467  derang0  24847  dfiota3  25760  uvcff  27208  iotain  27585  dfaimafn2  27997  rnfdmpr  28069  csbsngVD  28942  lineset  30472
  Copyright terms: Public domain W3C validator