I don't believe it's written up anywhere.
edit: in the comments Charlie Frohman corrects me:
Elementary moves for higher dimensional knots. (English summary)
Fund. Math. 184 (2004), 291–310.
57R40 (57R45 57R52)
has a proof similar in flavour to the sketch below. Thanks Charlie!
The idea is pretty simple, but maybe a bit of a pain to write up completely. Say $f : [0,1] \times S^1 \to \mathbb R^3$ is a smooth isotopy. Let $\pi : \mathbb R^3 \to \mathbb R^2$ be orthogonal projection onto a 2-dimensional subspace. $\pi \circ f : [0,1] \times S^1 \to \mathbb R^2$ is a 1-parameter family of (possibly singular) knot diagrams, but we can assume that at the initial and terminal parts of the family are regular knot diagrams.
The next step is to check the co-dimensions of the various types of singularities such maps can have.
For example, a knot has its derivative. That derivative is "vertical" is a co-dimension 2 condition on a vector. Since a knot is 1-dimensional, it's a co-dimension 1 condition on the knot. Such a vertical derivative for $f$ results in its projection to $\mathbb R^2$ to have a cusp. So a generic knot diagram has no cusps, but a 1-parameter family will have a finite number of cusps, and these appear as Reidemeister moves of "type 1". Technically, this is a formulation of Whitney's theorem that maps between 2-manifolds generically only have fold and cusp-type singularities.
Further, you can ask about double, triple and multiple-points for the projections, non-transverse double points, and so on. Double points are generic but triple-points are co-dimension 2, and $n$-tuple points are co-dimension $2(n-2)$ in general, so you generically can avoid anything worse than triple points. This gives the Reidemeister "type 3" moves. Tangential double points are also co-dimension 2, and generic such ones produce Reidemeister "type 2" moves.
As you can see this isn't quite a full proof using only the technology of Guillemin and Pollack, meaning it's not quite just Sard's theorem that we're using. We're really using the "Multijet transversality" type theorem, like Theorem 4.13 from Golubitsky and Guillemin. But I suspect like Whitney's work "The general type of singularity of a set of $2n-1$ functions of $n$ variables" you should be able to massage the above into a solid argument without dredging up too much formalism.
edit: I do think there is likely a "smart" proof of this that avoids jet transversality. For example, check out Milnor's proof that Morse functions are dense in the space of smooth functions $M \to \mathbb R$ (in Milnor's Morse Theory text). You'd think in principle you'd have to use jet transversality for this but by picking a diverse-enough family of functions to start with, he pulls it all back to the level of Sard's Theorem. I think there should be a similarly slick proof of Reidemeister's theorem, using only Sard's Theorem.