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.
The formula in df-clel (restated below) states that only those classes for which E. x x = A holds can be members of classes. Thus, a member of a class is always equal to a set, which excludes proper classes from class membership.
As explained in wl-cleq-4 , item 3, E. x x = A is a sufficient criterion for a class to be a set, provided that Leibniz's Law holds for equality. Therefore this axiom is often rephrased as: classes contain only sets as members.
**Principles of equality**
Using this axiom we can derive the class-level counterparts of ax-8 (see eleq2 ) and ax-9 (see eleq1 ). Since ax-wl-cleq already asserts that equality between classes is an equivalence relation, the operators = and e. alone cannot distinguish equal classes. Hence, if membership is the only property that matters for classes, Leibniz's Law will hold. Later, however, additional class builders may introduce further properties of classes. A conservativity check for such builders can ensure this does not occur.
**Eliminability**
If we replace the class variable A with a set variable z in this axiom, the auxiliary variable x can be eliminated, leaving only the trivial result ( z e. B <-> z e. B ) . Thus, df-clel by itself does not determine when a set is a member of a class. From this perspective, df-clel is in fact an axiom in disguise and would more appropriately be called ax-clel.
Overall, our axiomization leaves the meaning of fundamental expressions x e. A or x e. B open. All other fundamental formulas of set theory ( A not a set variable, A e. B , x = B A = B ) can be reduced solely to the basic formulas x e. A or x e. B .
If an axiomatization leaves a fundamental formula like x e. A unspecified, we could in principle define it bi-conditionally by any formula whatsoever - for example, the trivial T. . This, however, is not the approach we take. Instead, an appropriate class builder such as df-clab fills this gap.
(Contributed by Wolf Lammen, 26-Aug-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax-wl-clel | ⊢ ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cA | ⊢ 𝐴 | |
| 1 | cB | ⊢ 𝐵 | |
| 2 | 0 1 | wcel | ⊢ 𝐴 ∈ 𝐵 |
| 3 | vx | ⊢ 𝑥 | |
| 4 | 3 | cv | ⊢ 𝑥 |
| 5 | 4 0 | wceq | ⊢ 𝑥 = 𝐴 |
| 6 | 4 1 | wcel | ⊢ 𝑥 ∈ 𝐵 |
| 7 | 5 6 | wa | ⊢ ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵 ) |
| 8 | 7 3 | wex | ⊢ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵 ) |
| 9 | 2 8 | wb | ⊢ ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) |