I think the condition "the appearance of B without X" can be changed to "the free appearance of B without X".

B can contain the constraint of X, when the constraint of B containing X appears, by eliminating quantifiers and so on.

The value formula can eliminate x in b, so that b does not contain x, thus satisfying the upper equivalence formula.