Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-sn | Structured version Visualization version 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, see snprc 4653. For an alternate definition see dfsn2 4580. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
df-sn | ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | csn 4567 | . 2 class {𝐴} |
3 | vx | . . . . 5 setvar 𝑥 | |
4 | 3 | cv 1536 | . . . 4 class 𝑥 |
5 | 4, 1 | wceq 1537 | . . 3 wff 𝑥 = 𝐴 |
6 | 5, 3 | cab 2799 | . 2 class {𝑥 ∣ 𝑥 = 𝐴} |
7 | 2, 6 | wceq 1537 | 1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} |
Colors of variables: wff setvar class |
This definition is referenced by: sneq 4577 elsng 4581 absn 4585 dfsn2ALT 4587 rabsssn 4607 csbsng 4644 pw0 4745 iunid 4984 uniabio 6328 dfimafn2 6729 fnsnfv 6743 suppvalbr 7834 snec 8360 0map0sn0 8449 infmap2 9640 cf0 9673 cflecard 9675 brdom7disj 9953 brdom6disj 9954 vdwlem6 16322 hashbc0 16341 symgbas0 18517 psrbagsn 20275 ptcmplem2 22661 snclseqg 22724 nmoo0 28568 nmop0 29763 nmfn0 29764 disjabrex 30332 disjabrexf 30333 pstmfval 31136 hasheuni 31344 derang0 32416 dfiota3 33384 bj-nuliotaALT 34354 poimirlem28 34935 lineset 36889 frege54cor1c 40281 iotain 40769 csbsngVD 41247 dfaimafn2 43385 dfatsnafv2 43471 rnfdmpr 43500 |
Copyright terms: Public domain | W3C validator |