| Description: This is essentially Axiom
ax-12 2216 weakened by additional restrictions on
variables. Besides axc11r 2400, this theorem should be the only one
referencing ax-12 2216 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 1945,
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.) |
