You will not find any substitution notation in Frege, altough he does have a rule of substitution in his *Grundgesetze*-system (namely, rule 9 of its § 48). For an early example of substition notation in logic, see Russell's paper *Mathematical Logic as based on the Theory of Types* (1908). For instance, on its page 238 you can read:

If *p* is a proposition, and *a* a constituent of *p*, let "*p/a;x*" denote the proposition which results from substituting *x* for *a* wherever *a* occurs in *p*.

Gödel, as cited above by Mauro Allegranza, probably takes his notation from Von Neumann, who in his remarkable paper *Zur Hilbertschen Beweistheorie* (1927) writes

$$\mathrm{Subst}\bigl(\begin{smallmatrix}
x_p \\ b
\end{smallmatrix} \bigr)a$$

Von Neumann may in turn have taken this notation from his fellow countryman Julius König's book *Neue Grundlagen der Logik, Arithmetik, und Mengenlehre* (1904). König explains his substitution notation,

$$\mathrm{S}\bigl(\begin{smallmatrix}
x \\ V
\end{smallmatrix} \bigr)F$$

on pages 92ff.

The source of König's notation may be the notation exemplified by

$$\begin{pmatrix}
1&2&3&4 \\
2&4&1&3
\end{pmatrix} $$

for what are nowadays usually called permutations, but which Cauchy, who introduced this notation in a paper from 1815, called, precisely, substitutions.

Substitution notation is of course also used in the calculus. Thus, Cauchy in his *Cours d'Analyse* (1821) suggests

$$\int f(x)\,dx\,\bigl[\begin{smallmatrix}
x=x_0 \\ x=X
\end{smallmatrix} \bigr]$$

as one possible notation for the integral. (The now standard notation $\int_{x_0}^Xf(x)\,dx$ was introduced by Fourier.) The relevant extracts from Cauchy's texts can be found, in the original and translated, in Jacqueline Stedall's source book *Mathematics Emerging*.

I should note that I have learned most of the information reported here from Per Martin-Löf (the reference to König is due to Göran Sundholm).

preciselythis notation, let me mention that Bourbaki introduces $(B|x)A$ in a draft of E.I, dating from 1951 (état 6, page 3) and keeps it since then. The preceding version uses the $(Sub$ $x|B)A$ (état 5, page 2). $\endgroup$operation. $\endgroup$