Axiom ax-wl-8cl 33377

Description: In ZFC, as presented in this document, classes are meant to be just a notational convenience, that can be reduced to pure set theory by means of df-clab 2609 (there stated in the eliminable property). That is, in an expression x e. A, the class variable A is implicitely assumed to represent an expression { z | ph } with some appropriate ph. Unfortunately, ph syntactically covers any well-formed formula (wff), including z e. A. This choice inevitably breaks the stated property. And it potentially carries over to any expression containing class variables. To fix this, a simple rule could exclude class variables at all in a class defining wff. A more elaborate rule could detect, and limit exclusion to proper classes (potentially problematic). In any case, the verification process should enforce any such rule during replacement, which it currently does not. The result is that we rely on the awareness of theorem designers to this problem. It seems, in ZFC proper classes are reduced to a few instances only, so a careful study may reveal that this limited use does not impose logical loop holes. It must be said, still, this necessary extra knowledge contradicts the general philosophy of Metamath, trying to establish certainty by a machine executable confirmation.

An extension to ZFC allows classes to exist on their own. Classes are then extensions to sets, also seamlessly extending the idea of elementhood. In order to move from the general to the specific, sets presuppose classes, so classes should be introduced first. This is somewhat in opposition to the classic order of introduction of syntactic elements, but has been carried out in the past, for example by the von-Neumann theory of classes.

In the context of Metamath, which is a purely text-based syntactical concept, no semantics are imposed at the very beginning on classes. Instead axioms will narrow down bit by bit how elementhood behaves in proofs, of course always with the intuitive understanding of a human in mind.

One basic property of elementhood we expect is that the 'element' is replaceable with something equal to it. Or that equality is finer grained than the elementhood relation. This idea is formally expressed in terms coined 'implicit substitution' in this document: ( ( x = y ) -> ( x e. A <-> y e. A ) ). This axiom prepares this notation.

Note that particular constructions of classes like that in df-clab 2609 in fact allow to prove this axiom. Can we expect to eliminate this axiom then? No, the generalizing term still refers to an unexplained subterm x e. A, so this axiom recurs in the general case. On the other hand, our axiom here stays true, even when just the existence of a class is known, as is often the case after applying the axiom of choice, without a chance to actually construct it.

We provide a version of this axiom, that requires all variables to be distinct. Step by step these restrictions are lifted, in the end covering the most general term A e. B.

This axiom is meant as a replacement for ax-8 1992. (Contributed by Wolf Lammen, 27-Nov-2021.)

Assertion

Ref	Expression
ax-wl-8cl	|- ( x = y -> ( x e. A -> y e. A ) )

Distinct variable group:   x, y, A

Detailed syntax breakdown of Axiom ax-wl-8cl

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar x
2		vy	. . 3 setvar y
3	1, 2	weq 1874	. 2 wff x = y
4		cA	. . . 4 class A
5	1, 4	wcel-wl 33373	. . 3 wff x e. A
6	2, 4	wcel-wl 33373	. . 3 wff y e. A
7	5, 6	wi 4	. 2 wff ( x e. A -> y e. A )
8	3, 7	wi 4	1 wff ( x = y -> ( x e. A -> y e. A ) )

This axiom is referenced by:  wl-ax8clv1  33378  wl-clelv2-just  33379