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

Definition df-sn 4030
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 4042. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
df-sn
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-sn
StepHypRef Expression
1 cA . . 3
21csn 4029 . 2
3 vx . . . . 5
43cv 1394 . . . 4
54, 1wceq 1395 . . 3
65, 3cab 2442 . 2
72, 6wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  sneq  4039  elsn  4043  elsncg  4052  csbsng  4088  rabsn  4097  pw0  4177  iunid  4385  dfiota2  5557  uniabio  5566  dfimafn2  5923  fnsnfv  5933  suppvalbr  6922  snec  7393  infmap2  8619  cf0  8652  cflecard  8654  brdom7disj  8930  brdom6disj  8931  vdwlem6  14504  hashbc0  14523  symgbas0  16419  psrbagsn  18160  ptcmplem2  20553  snclseqg  20614  nmoo0  25706  nmop0  26905  nmfn0  26906  disjabrex  27443  disjabrexf  27444  pstmfval  27875  hasheuni  28091  derang0  28613  dfiota3  29573  iotain  31324  dfaimafn2  32251  rnfdmpr  32308  rabeqsn  32919  rabsssn  32920  csbsngVD  33693  bj-nuliotaALT  34587  lineset  35462  frege54cor1c  37942
  Copyright terms: Public domain W3C validator