Also have a look at Tips:_Writing_Models_for_ProB.
Classical B only has a LET substitution, no let construct for predicates or expressions. Event-B has no let construct whatsoever.
#x.(x=E & P)
corresponds to something like
let x=E in P
dom({x,y|y=E & P})
corresponds to something like
{x|let y=E in P}
#UNION(x).(x=E|F)
corresponds to something like
let x=E in F