I missed this question but I still want to have my say as I think this deserves to be better known. Perhaps this would make a good topic for a blog post? This is, I think, Poincare's proof of a strong form of the PBW theorem. Birkoff and Witt proved a weaker result a couple of decades later. This story is told in this reference:

MR1793103 (2001f:01039) Ton-That, Tuong ; Tran, Thai-Duong . Poincaré's proof of the so-called Birkhoff-Witt theorem. Rev. Histoire Math. 5 (1999), no. 2, 249--284 (2000).

The set-up is given in Torsten's answer. We have a symmetric monoidal category enriched in the category of vector spaces over a field of characteristic zero. We also assume we can form countable direct sums and that idempotents have images (this is no loss of generality as the original category can be formaly enlarged if necessary). This gives the structure and there is a long list of compatibility conditions most of which should be obvious. I am not sure if we require the tensor product to be distributive over countable direct sums.

Just to be clear I do not assume we have cokernels and I have in mind examples where cokernels do not exist.

However let's start in the category of vector spaces. I was given a copy of notes taken at a talk by Kostant in France in the 1975. The only references I know of are the following (both of which make the construction seem obscure).

MR2301242 (2008d:17015) Durov, Nikolai ; Meljanac, Stjepan ; Samsarov, Andjelo ; Škoda, Zoran . A universal formula for representing Lie algebra generators as formal power series with coefficients in the Weyl algebra. J. Algebra 309 (2007), no. 1, 318--359.

http://arxiv.org/abs/math/0604096

MR1991464 (2004f:17026) Petracci, Emanuela . Universal representations of Lie algebras by coderivations. Bull. Sci. Math. 127 (2003), no. 5, 439--465.

Anyway the basic idea is that we take the symmetric algebra $S(g)$ and define an action of $g$. This then generates the action of $U(g)$ and so constructs $U(g)$. In order to define the action of $g$ it is sufficient to define $x*y^n$ since we obtain the action of $x$ by polarisation. The key is that this is given by:

$$x*y^n = \sum_{j=0}^n \binom{n}{j}B_j ad^j(y)(x)y^{n-j}$$

where the $B_j$ are the Bernoulli numbers with generating function $x/(e^x-1)$.

Once you unwind this you find that you have constructed maps $S^r(g)\otimes S^s(g)\rightarrow S^{r+s-j}(g)$ for $r,s,j\ge 0$ by universal formulae. These formulae then make sense in the abstract setting.

I would be delighted to see a good exposition of this.

I missed this question but I still want to have my say as I think this deserves to be better known. Perhaps this would make a good topic for a blog post? This is, I think, Poincare's proof of a strong form of the PBW theorem. Birkoff and Witt proved a weaker result a couple of decades later. This story is told in this reference:

MR1793103 (2001f:01039) Ton-That, Tuong ; Tran, Thai-Duong . Poincaré's proof of the so-called Birkhoff-Witt theorem. Rev. Histoire Math. 5 (1999), no. 2, 249--284 (2000).

The set-up is given in Torsten's answer. We have a symmetric monoidal category enriched in the category of vector spaces over a field of characteristic zero. We also assume we can form countable direct sums and that idempotents have images (this is no loss of generality as the original category can be formaly enlarged if necessary). This gives the structure and there is a long list of compatibility conditions most of which should be obvious. I am not sure if we require the tensor product to be distributive over countable direct sums.

Just to be clear I do not assume we have cokernels and I have in mind examples where cokernels do not exist.

However let's start in the category of vector spaces. I was given a copy of notes taken at a talk by Kostant in France in the 1975. The only references I know of are the following (both of which make the construction seem obscure).

MR2301242 (2008d:17015) Durov, Nikolai ; Meljanac, Stjepan ; Samsarov, Andjelo ; Škoda, Zoran . A universal formula for representing Lie algebra generators as formal power series with coefficients in the Weyl algebra. J. Algebra 309 (2007), no. 1, 318--359.

http://arxiv.org/abs/math/0604096

MR1991464 (2004f:17026) Petracci, Emanuela . Universal representations of Lie algebras by coderivations. Bull. Sci. Math. 127 (2003), no. 5, 439--465.

Anyway the basic idea is that we take the symmetric algebra $S(g)$ and define an action of $g$. This then generates the action of $U(g)$ and so constructs $U(g)$. In order to define the action of $g$ it is sufficient to define $x*y^n$ since we obtain the action of $x$ by polarisation. The key is that this is given by:

$$x*y^n = \sum_{j=0}^n \binom{n}{j}B_j ad^j(y)(x)y^{n-j}$$

where the $B_j$ are the Bernoulli numbers with generating function $x/(e^x-1)$.

Once you unwind this you find that you have constructed maps $S^r(g)\otimes S^s(g)\rightarrow S^{r+s-j}(g)$ for $r,s,j\ge 0$ by universal formulae. These formulae then make sense in the abstract setting.

I would be delighted to see a good exposition of this.

Edit: The following reference looks as though it should be relevant but I didn't get much from it.

MR1894038 (2003b:17014) Cortiñas, Guillermo . An explicit formula for PBW quantization. Comm. Algebra 30 (2002), no. 4, 1705--1713.