Description: Every setvar is a member of { x | T. } , which is therefore "a"
universal class. Once class extensionality dfcleq is available, we can
say "the" universal class (see df-v ). This is sbtru expressed using
class abstractions. (Contributed by BJ, 2-Sep-2023)