![]() |
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 4720. For an alternate definition see dfsn2 4640. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
df-sn | ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | csn 4627 | . 2 class {𝐴} |
3 | vx | . . . . 5 setvar 𝑥 | |
4 | 3 | cv 1540 | . . . 4 class 𝑥 |
5 | 4, 1 | wceq 1541 | . . 3 wff 𝑥 = 𝐴 |
6 | 5, 3 | cab 2709 | . 2 class {𝑥 ∣ 𝑥 = 𝐴} |
7 | 2, 6 | wceq 1541 | 1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} |
Colors of variables: wff setvar class |
This definition is referenced by: sneq 4637 elsng 4641 absn 4645 dfsn2ALT 4647 rabsssn 4669 csbsng 4711 pw0 4814 iunidOLD 5063 uniabio 6507 iotaval 6511 dfimafn2 6952 fnsnfvOLD 6968 suppvalbr 8146 snec 8770 fset0 8844 0map0sn0 8875 infmap2 10209 cf0 10242 cflecard 10244 brdom7disj 10522 brdom6disj 10523 vdwlem6 16915 hashbc0 16934 symgbas0 19250 psrbagsn 21615 ptcmplem2 23548 snclseqg 23611 nmoo0 30031 nmop0 31226 nmfn0 31227 disjabrex 31800 disjabrexf 31801 pstmfval 32864 hasheuni 33071 derang0 34148 dfiota3 34883 bj-nuliotaALT 35927 poimirlem28 36504 lineset 38597 abbi1sn 41036 frege54cor1c 42651 iotain 43161 csbsngVD 43639 dfaimafn2 45860 dfatsnafv2 45946 rnfdmpr 45975 |
Copyright terms: Public domain | W3C validator |