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

Definition df-sn 3648
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 3656. (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 3642 . 2  class  { A }
3 vx . . . . 5  set  x
43cv 1624 . . . 4  class  x
54, 1wceq 1625 . . 3  wff  x  =  A
65, 3cab 2271 . 2  class  { x  |  x  =  A }
72, 6wceq 1625 1  wff  { A }  =  { x  |  x  =  A }
Colors of variables: wff set class
This definition is referenced by:  sneq  3653  elsn  3657  elsncg  3664  csbsng  3694  rabsn  3699  pw0  3764  iunid  3959  dfiota2  5222  uniabio  5231  dfimafn2  5574  fnsnfv  5584  snec  6724  infmap2  7846  cf0  7879  cflecard  7881  brdom7disj  8158  brdom6disj  8159  vdwlem6  13035  hashbc0  13054  psrbagsn  16238  ptcmplem2  17749  snclseqg  17800  nmoo0  21371  nmop0  22568  nmfn0  22569  disjabrex  23361  disjabrexf  23362  hasheuni  23455  derang0  23702  dfiota3  24464  uvcff  27251  iotain  27628  dfaimafn2  28039  csbsngVD  28742  lineset  30000
  Copyright terms: Public domain W3C validator