Axiom ax-wl-cleq

Description: Disclaimer: The material presented here is just my (WL's) personal perception. I am not an expert in this field, so some or all of the text here can be misleading, or outright wrong.

This text should be read as an exploration rather than as a definite statement, open to doubt, alternatives, and reinterpretation.

At the point where df-cleq is introduced, the foundations of set theory are being established through the notion of a class. A central property of classes is what elements, expressed by the membership operator e. , belong to them . Quantification ( A. x ) applies only to objects that a variable of kind setvar can represent. These objects will henceforth be called sets. Some classes may not be sets; these are called proper classes. It remains open at this stage whether membership can involve them.

The formula given in df-cleq (restated below) asserts that two classes are equal if and only if they have exactly the same sets as elements. If proper classes are also admitted as elements, then two equal classes could still differ by such elements, potentially violating Leibniz's Law. A future axiom df-clel addresses this issue; df-cleq alone does not.

**Primitive connectives and class builders**

Specially crafted primitive operators on classes or class builders could introduce properties of classes beyond membership, not reflected in the formula here. This again risks violating Leibniz's Law. Therefore, the introduction of any future primitive operator or class builder must include a conservativity check to ensure consistency with Leibniz's Law.

**This axiom covers only some principles of equality**

The notion of equality expressed in this axiom does not automatically coincide with the general notion of equality. Some principles are, however, already captured: Equality is shown to be an equivalence relation, covering transivity ( eqtr ), reflexivity ( eqid ) and symmetry ( eqcom ). It also yields the class-level version of ax-ext (the backward direction of df-cleq ) holds.

If we assume x = A holds, then substituting the free set variable y with A in ax6ev and ax12v2 yields provable theorems (see wl-isseteq , and wl-ax12v2cl ). However, a bound variable cannot be replaced with a class variable, since quantification over classes is not permitted. Taken together with the results from the previous paragraph, this shows that a class variable equal to a set behaves the same as a set variable, provided it is not quantified.

**Conservativity**

Moreover, this axiom is already partly derivable if all class variables are replaced by variables of type "setvar". In that case, the statement reduces to an instance of axextb . This shows that the class builder cv is consistent with this axiom.

**Eliminable operator**

Finally, this axiom supports the idea that proper classes, and operators between them, should be eliminable, as required by ZF: It reduces equality to their membership properties. However, since the term x e. A is still undefined, elimination reduces equality to just something not yet clarified.

**Axiom vs Definition**

Up to this point, the only content involving class variables comes from the syntax definitions wceq and wcel . Axioms are therefore required to progressively refine the semantics of classes until provable results coincide with our intended conception of set theory. This refinement process is explained in Step 4 of wl-cleq-2 .

From this perspective, df-cleq is in fact an axiom in disguise and would more appropriately be named ax-cleq.

At first glance, one might think that A = B is defined by the right-hand side of the biconditional. This would make x e. A , i.e. membership of a set in a class, the more primitive concept, from which equality of classes could be derived. Such a viewpoint would be coherent if the properties of membership could be fully determined by other axioms. In my (WL's') opinion, however, the more direct and fruitful approach is not to construct class equality from membership, but to treat equality itself as axiomatic.

(Contributed by Wolf Lammen, 25-Aug-2025)

	Ref	Expression
Assertion	ax-wl-cleq	$$⊢A=B\leftrightarrow \forall x\left(x\in A\leftrightarrow x\in B\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2	0 1	wceq	$$wffA=B$$
3		vx	$$setvarx$$
4	3	cv	$$setvarx$$
5	4 0	wcel	$$wffx\in A$$
6	4 1	wcel	$$wffx\in B$$
7	5 6	wb	$$wff\left(x\in A\leftrightarrow x\in B\right)$$
8	7 3	wal	$$wff\forall x\left(x\in A\leftrightarrow x\in B\right)$$
9	2 8	wb	$$wff\left(A=B\leftrightarrow \forall x\left(x\in A\leftrightarrow x\in B\right)\right)$$