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

Definition df-sn 3381
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 3389. (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 3375 . 2 class {𝐴}
3 vx . . . . 5 setvar 𝑥
43cv 1242 . . . 4 class 𝑥
54, 1wceq 1243 . . 3 wff 𝑥 = 𝐴
65, 3cab 2026 . 2 class {𝑥𝑥 = 𝐴}
72, 6wceq 1243 1 wff {𝐴} = {𝑥𝑥 = 𝐴}
Colors of variables: wff set class
This definition is referenced by:  sneq  3386  elsng  3390  csbsng  3431  rabsn  3437  pw0  3511  iunid  3712  dfiota2  4868  uniabio  4877  dfimafn2  5223  fnsnfv  5232  snec  6167  bdcsn  9990
  Copyright terms: Public domain W3C validator