Description: Lemma for bj-vtoclg1f1 (an instance of this lemma is a version of bj-vtoclg1f1 where x and y are identified). (Contributed by BJ, 30-Apr-2019) (Proof modification is discouraged.)