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 3511. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
df-sn | ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | csn 3497 | . 2 class {𝐴} |
3 | vx | . . . . 5 setvar 𝑥 | |
4 | 3 | cv 1315 | . . . 4 class 𝑥 |
5 | 4, 1 | wceq 1316 | . . 3 wff 𝑥 = 𝐴 |
6 | 5, 3 | cab 2103 | . 2 class {𝑥 ∣ 𝑥 = 𝐴} |
7 | 2, 6 | wceq 1316 | 1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} |
Colors of variables: wff set class |
This definition is referenced by: sneq 3508 elsng 3512 csbsng 3554 rabsn 3560 pw0 3637 iunid 3838 dfiota2 5059 uniabio 5068 dfimafn2 5439 fnsnfv 5448 snec 6458 bdcsn 12964 |
Copyright terms: Public domain | W3C validator |