Well, this an easy one! You, simply, do NOT write "let" in (symbolic) logic, as you do it in the vernacular (in your mother-tongue, for instance)!
Now, the so called "mathematical vernacular" [WOT, in Dutch] has been explained (and codified) long ago, by one of my Dutch math teachers, N. G. [ = Dick ] de Bruijn, of the Eindhoven Polytechnics [TUE], The Netherlands, in lectures (on "[De] Taal en Structuur van de Wiskunde" [= The language and structure of mathematics]), sometime during the late seventies, to be precise. (Cf., e.g., Euclides 55, 1979-1980.) --
There is even a nice book (in Dutch) on this, authored by one of his former PhD students and collaborators, Rob Nederpelt (Eindhoven) :
“De taal van de wiskunde, Een verkenning van wiskundig taalgebruik en logische redeneerpatronen” [The language of mathematics, An exploration of the mathematical use of language and the logical proof-patterns] (With an introduction by Dirk van Dalen), Versluis, Almere 1987.
Unfortunately, Rob's book has not been translated so far. But see his recent Cambridge-UP-monograph, co-authored with Herman Geuvers [Radboud Univ., Nijmegen], on "Automath" and the like: "Type Theory and Formal Proof. An Introduction", Cambridge University Press, Cambridge, 2014 [ISBN 978-1-107-03650-5, xxviii + 436 pages] etc.
Essentially, an Automath "language" / system (of proof checking mathematical texts) amounts to a very formal way of writing down a WOT- / "mathematical vernacular"-text, such as to be readable by a machine, a computer, say.
In Automath (and the like), the informal "let" goes either into
(1) a [meta] variable-declaration
or else into
(2) an explicit definition,
pointing out to two distinct -- rather tricky -- ways of manipulating textual substitutions in actual mathematics. (There is third way of doing "substitutions" in logic / mathematics, by applying the so-called CUT-rule of Gerhard Gentzen [1935]; this is just a way of codifying the usual practice of "proving by lemmas" in Euclid & so on.)
For the rest -- if (still) Dutchless and unable to read Rob's WOT-book of 1987 --, I'd suggest buying the recent monograph mentioned above: it is aimed at undergraduates and, as a bonus, it covers a lot of technical stuff you won't easily find elsewhere in print...