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

Definition df-sn 3437
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 3445. (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 3431 . 2 class {𝐴}
3 vx . . . . 5 setvar 𝑥
43cv 1286 . . . 4 class 𝑥
54, 1wceq 1287 . . 3 wff 𝑥 = 𝐴
65, 3cab 2071 . 2 class {𝑥𝑥 = 𝐴}
72, 6wceq 1287 1 wff {𝐴} = {𝑥𝑥 = 𝐴}
Colors of variables: wff set class
This definition is referenced by:  sneq  3442  elsng  3446  csbsng  3486  rabsn  3492  pw0  3567  iunid  3768  dfiota2  4947  uniabio  4956  dfimafn2  5317  fnsnfv  5326  snec  6305  bdcsn  11206
  Copyright terms: Public domain W3C validator