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

Definition df-sn 3915
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 , although it is not very meaningful in this case. For an alternate definition see dfsn2 3923. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
df-sn
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-sn
StepHypRef Expression
1 cA . . 3
21csn 3909 . 2
3 vx . . . . 5
43cv 1669 . . . 4
54, 1wceq 1670 . . 3
65, 3cab 2475 . 2
72, 6wceq 1670 1
Colors of variables: wff set class
This definition is referenced by:  sneq  3920  elsn  3924  elsncg  3932  csbsng  3967  rabsn  3973  pw0  4045  iunid  4251  dfiota2  5402  uniabio  5411  dfimafn2  5757  fnsnfv  5767  snec  7129  infmap2  8269  cf0  8302  cflecard  8304  brdom7disj  8580  brdom6disj  8581  vdwlem6  13894  hashbc0  13913  symgbas0  15680  psrbagsn  17180  uvcff  17737  ptcmplem2  19099  snclseqg  19160  nmoo0  23313  nmop0  24512  nmfn0  24513  disjabrex  25054  disjabrexf  25055  pstmfval  25502  hasheuni  25714  derang0  26203  dfiota3  27107  iotain  28845  dfaimafn2  29251  rnfdmpr  29330  csbsngVD  30475  lineset  32085
  Copyright terms: Public domain W3C validator