Description: One of four lemmas for nonfreeness: antecedent expressed with existential quantifier and consequent expressed with universal quantifier. (Contributed by BJ, 12-Aug-2023) (Proof modification is discouraged.)