at the first occurrence of "first-order logic", I mention the common abbreviation "FOL"
in the comment of df-clab, I clarify "the LHS (definiendum)" to "the definiendum (the left-hand side of the
biconditional), and I spell out the second occurrence of "LHS".
at the first comment having "LHS" and "RHS", I give their meanings.
Following @wlammen's remarks in https://github.com/metamath/set.mm/pull/4003#discussion_r1609933523, I spelt out some abbreviations: