Description: This is essentially axiom
ax-12 2047 weakened by additional restrictions on
variables. Besides axc11r 2187, this theorem should be the only one
referencing ax-12 2047 directly.
Both restrictions on variables have their own value. If for a moment we
assume could be
set to , then, after
elimination of the
tautology , immediately we have for all
and , that is ax-5 1839,
a degenerate result.
The second restriction is not necessary, but a simplification that makes
the following interpretation easier to see. Since textually at
most depends on , we can look at it at some given 'fixed' .
This theorem now states that the truth value of will stay
constant, as long as we 'vary around '
only such that
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 is possible at all. Note
that Metamath is a text processor that easily sees a difference between
text chunks
and . 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 run
through all textual representations of sets.
Had we allowed to depend also on , 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.) |