Theorem wl-cleq-6 37496

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 definite statements, open to doubt, alternatives, and reinterpretation.

Eliminability of classes

One requirement of Zermelo-Fraenkel set theory (ZF) is that it can be formulated without referring to classes. Since set.mm implements ZF, it must therefore be possible to eliminate all classes.

This has two main implications.

First, every class builder other than cv 1538 must be a definition, making its elimination straightforward. The class abstraction df-clab 2715 is a special case: it reduces the primitive expression 𝑥 ∈ {𝑦 ∣ 𝜑} to a first-order logic (FOL) predicate. Other class expressions, such as 𝐴 = 𝐵 or 𝐴 ∈ 𝐵, can ultimately be reduced to occurrences of 𝑥 ∈ 𝐴. Hence, if a class variable 𝐴 represents only class abstractions, some groundwork for eliminability is already established.

Since set variables themselves can be expressed as class abstractions - namely 𝑥 = {𝑦 ∣ 𝑦 ∈ 𝑥} (see cvjust 2731) - this formulation does not conflict with the use of class builder cv 1538.

Second, substituting a class abstraction for a class variable 𝐴 must not introduce a recursion. The predicate used in the abstraction must not depend on class variables again. Under this restriction, a finite number of elimination steps will reduce the class variable 𝐴 to a term expressed purely in FOL, without classes.

These conditions apply only to substitution. The expression 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴} (abid1 2878) is a valid and provable equation, and it should not be interpreted as an assignment that binds a particular instance to 𝐴.

(Contributed by Wolf Lammen, 13-Oct-2025.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem wl-cleq-6

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2729

This theorem is referenced by: (None)