Let t1[x:=t0] denote the result of substituting all occurrences of variable x in term t1 with the term t0. These rules define substitution recursively:

x[x:=t0] = t2
y[x:=t0] = y   (for any variable y distinct from x)
c[x:=t0] = c   (for any constant symbol c)
f(t1,...,tn)[x:=t0] = f(t1[x:=t0],...,tn[x:=t0])

The first cases are base cases and the last case is recursive case.

For quantifier-free formulas, we similarly substitute recursively. We rename quantified variables along the way to make them distinct from other variables (this avoides accidental “variable capture”):

R(t1,...,tn)[x:=t0] = R(t1[x:=t0],...,tn[x:=t0])
(t1=t2)[x:=t0] = (t1[x:=t0] = t2[x:=t0])
(F1 & F2)[x:=t0] = (F1[x:=t0] & F2[x:=t0])
(~F)[x:=t0] = ~(F[x:=t0])
(forall y. F) [x:=t0]  =  forall y. (F[x:=t0]),   if y does not occur in t (otherwise, rename y as a bound variable)
(exists y. F) [x:=t0]  =  exists y. (F[x:=t0]),   if y does not occur in t (otherwise, rename y as a bound variable)