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.
For predicates this encodes a let predicate:
#x.(x=E & P)
corresponds to something like
let x=E in P
Within set comprehensions one can use the following construct:
dom({x,y|y=E & P})
corresponds to something like
{x|let y=E in P}
In case F is a set expression, then the following construct can be used to encode a let statement:
#UNION(x).(x=E|F)
corresponds to something like
let x=E in F
The following construct has exactly the same effect:
#INTER(x).(x=E|F)
Classical B only has an IF-THEN-ELSE substitution (aka statement), no such construct for predicates or expressions.
%((x).(x=0 & PRED|C1)\/%(x).(x=0 & not(PRED)|C2)) (0)
encodes
if PRED then C1 else C2