|Description: Candidate definition for
df-clel 2647 (the need for it is exposed in
bj-ax8 33012). The similarity of the hypothesis and the
together with all possible dv conditions, makes it clear that this
definition merely extends to class variables something that is true for
setvar variables, hence is conservative. This definition should be
directly referenced only by bj-dfclel 33014, which should be used instead.
The proof is irrelevant since this is a proposal for an axiom.
Note: the current definition df-clel 2647 already mentions cleljust 2038 as a
justification; here, we merely propose to put it (more preciesly: its
universal closure) as a hypothesis to make things more explicit.
(Contributed by BJ, 27-Jun-2019.)
(Proof modification is discouraged.)