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

Definition df-sn 3847
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 3855. (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 3841 . 2
3 vx . . . . 5
43cv 1653 . . . 4
54, 1wceq 1654 . . 3
65, 3cab 2429 . 2
72, 6wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  sneq  3852  elsn  3856  elsncg  3863  csbsng  3895  rabsn  3901  pw0  3973  iunid  4176  dfiota2  5465  uniabio  5474  dfimafn2  5824  fnsnfv  5834  snec  7016  infmap2  8149  cf0  8182  cflecard  8184  brdom7disj  8460  brdom6disj  8461  vdwlem6  13405  hashbc0  13424  psrbagsn  16606  ptcmplem2  18135  snclseqg  18196  nmoo0  22343  nmop0  23540  nmfn0  23541  disjabrex  24073  disjabrexf  24074  pstmfval  24340  hasheuni  24524  derang0  24959  dfiota3  25872  uvcff  27396  iotain  27773  dfaimafn2  28185  rnfdmpr  28265  csbsngVD  29246  lineset  30775
  Copyright terms: Public domain W3C validator