Metamath Proof Explorer


Theorem wl-cleq-6

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 must be a definition, making its elimination straightforward. The class abstraction df-clab is a special case: it reduces the primitive expression x e. { y | ph } to a first-order logic (FOL) predicate. Other class expressions, such as A = B or A e. B , can ultimately be reduced to occurrences of x e. A . Hence, if a class variable A represents only class abstractions, some groundwork for eliminability is already established.

Since set variables themselves can be expressed as class abstractions - namely x = { y | y e. x } (see cvjust ) - this formulation does not conflict with the use of class builder cv .

Second, substituting a class abstraction for a class variable A 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 A to a term expressed purely in FOL, without classes.

These conditions apply only to substitution. The expression A = { x | x e. A } ( abid1 ) is a valid and provable equation, and it should not be interpreted as an assignment that binds a particular instance to A .

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

Ref Expression
Assertion wl-cleq-6 A = B x x A x B

Proof

Step Hyp Ref Expression
1 dfcleq A = B x x A x B