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

Definition df-sn 3820
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 3828. (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 3814 . 2  class  { A }
3 vx . . . . 5  set  x
43cv 1651 . . . 4  class  x
54, 1wceq 1652 . . 3  wff  x  =  A
65, 3cab 2422 . 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  3825  elsn  3829  elsncg  3836  csbsng  3867  rabsn  3873  pw0  3945  iunid  4146  dfiota2  5419  uniabio  5428  dfimafn2  5776  fnsnfv  5786  snec  6967  infmap2  8098  cf0  8131  cflecard  8133  brdom7disj  8409  brdom6disj  8410  vdwlem6  13354  hashbc0  13373  psrbagsn  16555  ptcmplem2  18084  snclseqg  18145  nmoo0  22292  nmop0  23489  nmfn0  23490  disjabrex  24024  disjabrexf  24025  pstmfval  24291  hasheuni  24475  derang0  24855  dfiota3  25768  uvcff  27217  iotain  27594  dfaimafn2  28006  rnfdmpr  28083  csbsngVD  29005  lineset  30535
  Copyright terms: Public domain W3C validator