New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-sn GIF version

Definition df-sn 3741
 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 3747. (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 3737 . 2 class {A}
3 vx . . . . 5 setvar x
43cv 1641 . . . 4 class x
54, 1wceq 1642 . . 3 wff x = A
65, 3cab 2339 . 2 class {x x = A}
72, 6wceq 1642 1 wff {A} = {x x = A}
 Colors of variables: wff setvar class This definition is referenced by:  sneq  3744  elsn  3748  elsncg  3755  csbsng  3785  rabsn  3790  iunid  4021  1cex  4142  pw0  4160  elp6  4263  unipw1  4325  dfeu2  4333  dfiota2  4340  uniabio  4349  nnc0suc  4412  ltfintrilem1  4465  nnadjoin  4520  tfinnn  4534  nulnnn  4556  phi011lem1  4598  fconstopab  4815  dfimafn2  5367  fnsnfv  5373  snec  5987  map0e  6023
 Copyright terms: Public domain W3C validator