This is essentially Axiom [ax-12] weakened by additional restrictions on variables. Besides axc11r, this theorem should be the only one referencing [ax-12] directly.

Both restrictions on variables have their own value. If for a moment we assume \( x \) could be set to \( y \), then, after elimination of the tautology \( y = y \), immediately we have ph -> A. y ph for all \( \varphi \) and \( y \), that is [ax-5], a degenerate result.

The second restriction is not necessary, but a simplification that makes the following interpretation easier to see. Since \( \varphi \) textually at most depends on \( x \), we can look at it at some given 'fixed' \( y \). This theorem now states that the truth value of \( \varphi \) will stay constant, as long as we 'vary \( x \) around \( y \) ' only such that \( x = y \) still holds. Or in other words, equality is the finest grained logical expression. If you cannot differ two sets by =, you won't find a whatever sophisticated expression that does. One might wonder how the described variation of \( x \) is possible at all. Note that Metamath is a text processor that easily sees a difference between text chunks { x | -. x = x } and { y | -. y = y }. Our usual interpretation is to abstract from textual variations of the same set, but we are free to interpret Metamath's formalism differently, and in fact let \( x \) run through all textual representations of sets.

Had we allowed \( \varphi \) to depend also on \( y \), this idea is both harder to see, and it is less clear that this extra freedom introduces effects not covered by other axioms. (Contributed by Wolf Lammen, 8-Aug-2020.)