Description: Candidate definition for
df-cleq 2764 (the need for it is exposed in
bj-ax9 33219). The similarity of the hypothesis
⊢
∀𝑢∀𝑣(𝑢 = 𝑣 ↔ ∀𝑤(𝑤 ∈ 𝑢 ↔ 𝑤 ∈ 𝑣)) and the
conclusion 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-dfcleq 33223, which should be used instead. The proof is
irrelevant
since this is a proposal for an axiom.
Another definition, which would give finer control, is actually the pair
of definitions where each has one implication of the present
biconditional as hypothesis and conclusion. They assert that
extensionality (respectively, the left-substitution axiom for the
membership predicate) extends from setvars to classes. (Contributed by
BJ, 24-Jun-2019.) (Proof modification is
discouraged.) |