Theorem wl-cleq-4 37485

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.

**Semantics of Equality**

In https://us.metamath.org/mpeuni/mmset.html#class some basic information is given about class variables, and what they are intended to represent. They range over so called class builders, i.e. definitions with type code "class". At this stage, only one such builder is explicitly available: cv 1536. Zermelo-Fraenkel set theory (ZF) introduces just one more in df-clab 2718.

Restricting ourselves to exactly these class builders is not necessary for fixing the general properties of equality between classes. Other models of set theory can still be supported at this point - even with an unlimited number of class builders. In line with the step-by-step approach of gradually closing in on ZF set theory, we introduce axioms of limited complexity, each addressing only a small number of properties.

1. **General properties of equality**

There is a broadly shared understanding of what equality between objects expresses, extending beyond mathematics or set theory. Equality must at least form an equivalence relation, where 𝑥, 𝑦, and 𝑧 are objects of the universe under consideration::

1a. Reflexivity 𝑥 = 𝑥

1b. Symmetry (𝑥 = 𝑦 → 𝑦 = 𝑥

1c. Transitivity ((𝑥 = 𝑦 ∧ 𝑥 = 𝑧) → 𝑦 = 𝑧)

In addition equality must obey the Identity of Indiscernables (Leibniz's Law). It states that distinct, or unequal, objects cannot share all the same properties. In set.mm properties are expressed by formulas. Thus equal objects must always behave the same, yielding the same results when substituted in formulas.

2. **Equality in First Order Logic (FOL)**

Let us now see how FOL captures these principles. Several axioms center on equality, namely ax-6 1967, ax-7 2007, ax-8 2110, ax-9 2118 and ax-12 2178, and ax-13 . In paractice, restricted versions with distinct variable conditions are used: ax6v 1968, ax12v 2179. The unrestricted axioms together with axiom ax-13 2380 allow elimination of distinct variable conditions, but this gain is considered too minor to justify their routine use.

Equality in FOL is formalized as follows:

2a. Equality as an equivalence relation is essentially covered by ax-7 2007.

2b. For the primitive ∈ operator, Leibniz's Law is captured by ax-8 2110 and ax-9 2118.

2c. Its general form is stated in sbequ12 2252.

2d. Implicit substitution: assuming Leibniz's Law for a particular expression, there are theorems that extend its validity to other, derived expressions. Frequently, the derived expression introduces quantification over the original one.

3. **Equality between classes**

We require Leibniz's Law to hold for equality between classes. For a mixed expression 𝑥 = 𝐴 the sethood of 𝐴 should follow from that of 𝑥. Thus, the equation 𝑥 = 𝐴 can be regarded as a criterion for the sethood of 𝐴. In ZF, where only sets exist, this is expressed instead by ∃𝑥𝑥 = 𝐴 stating the existence of 𝐴 in the same fashion that the restricted axiom ax6ev 1969 does for set variables.

Equality between classes must still be an equivalence relation. It must also be conservative, meaning that the results described in 2. remain valid when both class variables in 𝐴 = 𝐵 are replaced by set variables. Assuming class variables are all sets, we require that ax6ev 1969, ax-7 , ax-8 , ax-9 and ax12v2 2180 are provable when free set variables are replaced by class variables. In this way, the assignment 𝑥 = 𝐴 can stand in for the syntactically impossible substitution of a set variable by a class variable, even if the class is known to contain a set.

Since in ZF we cannot quantify over a class variables, no pure class-based version of the quantified FOL axioms exist. Moreover, in ZF classes are not considered an integral part of the theory, so they need to be eliminable. This also impacts the treatment of equality if it is regarded as a primitive operation.

(Contributed by Wolf Lammen, 18-Sep-2025.)

Assertion

Ref	Expression
wl-cleq-4	⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem wl-cleq-4

Step	Hyp	Ref	Expression
1		dfcleq 2733	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 206  ∀wal 1535   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by: (None)