Description: Biconditional showing two possible (dual) definitions of substitution df-sb not using dummy variables. (Contributed by BJ, 19-Mar-2021)