Description: A more general version of cbvrabv . Usage of this theorem is discouraged because it depends on ax-13 . Use of cbvrabv2w is preferred. (Contributed by Glauco Siliprandi, 23-Oct-2021) (New usage is discouraged.)