HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-sn 2402
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 2410.
Assertion
Ref Expression
df-sn |- {A} = {x | x = A}
Distinct variable group:   x,A

Detailed syntax breakdown of Definition df-sn
StepHypRef Expression
1 cA . . 3 class A
21csn 2399 . 2 class {A}
3 vx . . . . 5 set x
43cv 952 . . . 4 class x
54, 1wceq 953 . . 3 wff x = A
65, 3cab 1456 . 2 class {x | x = A}
72, 6wceq 953 1 wff {A} = {x | x = A}
Colors of variables: wff set class
This definition is referenced by:  sneq 2407  elsn 2411  rabsn 2435  pw0 2459  moabex 2756  dmsnop 3317  dfimafn2 3747  fnsnfv 3752  oarec 4180  snec 4280  map0e 4326  pw2en 4426  abfii2 4536  abfii4 4538  brdom7disj 4776  brdom6disj 4777  cf0 4882  cflecard 4884  cfom 4888  sqr0 6602  infxpidmlem9 7503  infmap2 7523  subbas 7586  nmo0 8383  nmop0 9826  nmfn0 9827
Copyright terms: Public domain