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

Definition df-sn 3780
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 3788. (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 3774 . 2  class  { A }
3 vx . . . . 5  set  x
43cv 1648 . . . 4  class  x
54, 1wceq 1649 . . 3  wff  x  =  A
65, 3cab 2390 . 2  class  { x  |  x  =  A }
72, 6wceq 1649 1  wff  { A }  =  { x  |  x  =  A }
Colors of variables: wff set class
This definition is referenced by:  sneq  3785  elsn  3789  elsncg  3796  csbsng  3827  rabsn  3833  pw0  3905  iunid  4106  dfiota2  5378  uniabio  5387  dfimafn2  5735  fnsnfv  5745  snec  6926  infmap2  8054  cf0  8087  cflecard  8089  brdom7disj  8365  brdom6disj  8366  vdwlem6  13309  hashbc0  13328  psrbagsn  16510  ptcmplem2  18037  snclseqg  18098  nmoo0  22245  nmop0  23442  nmfn0  23443  disjabrex  23977  disjabrexf  23978  pstmfval  24244  hasheuni  24428  derang0  24808  dfiota3  25676  uvcff  27108  iotain  27485  dfaimafn2  27897  rnfdmpr  27964  csbsngVD  28714  lineset  30220
  Copyright terms: Public domain W3C validator