ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-sn GIF version

Definition df-sn 3412
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 3420. (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 class 𝐴
21csn 3406 . 2 class {𝐴}
3 vx . . . . 5 setvar 𝑥
43cv 1284 . . . 4 class 𝑥
54, 1wceq 1285 . . 3 wff 𝑥 = 𝐴
65, 3cab 2068 . 2 class {𝑥𝑥 = 𝐴}
72, 6wceq 1285 1 wff {𝐴} = {𝑥𝑥 = 𝐴}
Colors of variables: wff set class
This definition is referenced by:  sneq  3417  elsng  3421  csbsng  3461  rabsn  3467  pw0  3540  iunid  3741  dfiota2  4898  uniabio  4907  dfimafn2  5255  fnsnfv  5264  snec  6233  bdcsn  10819
  Copyright terms: Public domain W3C validator