![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-sn | GIF version |
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.) |
Ref | Expression |
---|---|
df-sn | ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | csn 3406 | . 2 class {𝐴} |
3 | vx | . . . . 5 setvar 𝑥 | |
4 | 3 | cv 1284 | . . . 4 class 𝑥 |
5 | 4, 1 | wceq 1285 | . . 3 wff 𝑥 = 𝐴 |
6 | 5, 3 | cab 2068 | . 2 class {𝑥 ∣ 𝑥 = 𝐴} |
7 | 2, 6 | wceq 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 |