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

Definition df-sn 3274
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 3282.
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 3270 . 2 class {A}
3 vx . . . . 5 set x
43cv 1614 . . . 4 class x
54, 1wceq 1615 . . 3 wff x = A
65, 3cab 2157 . 2 class {x | x = A}
72, 6wceq 1615 1 wff {A} = {x | x = A}
Colors of variables: wff set class
This definition is referenced by:  sneq 3279  elsn 3283  elsncg 3289  csbsng 3311  rabsn 3316  pw0 3357  iunid 3513  moabex 3708  dfimafn2 4846  fnsnfv 4851  fvopab6 4882  dfiota2 5260  uniabio 5269  oarec 5447  snec 5559  map0e 5605  pw2en 5714  abfii2 5918  abfii4 5920  cf0 6337  cflecard 6339  cfom 6344  brdom7disj 6454  brdom6disj 6455  cfomOLD 6525  sqr0 8422  infxpidmlem9OLD 9359  infmap2 9380  subbas 9915  nmo0 10814  zrdivrng 11414  nmop0 12537  nmfn0 12538  subspemp 15926  singempcon 16004  idtrgrp 16017  pi1bval 17173  iotain 17466  csbsngVD 17812  lineset 18443
Copyright terms: Public domain