| Description: Version of equsalv 2304 with a disjoint variable condition, and of equsal 2450
with two disjoint variable conditions, which requires fewer axioms. See
also the dual form equsexvw 2027.
This theorem lays the foundation to a transformation of expressions
called substitution of set variables in a wff. Only in this particular
context we additionally assume 𝜑 and 𝑦 disjoint, stated here as
𝜑(𝑥). Similarly the disjointness of
𝜓 and
𝑥
is
expressed by 𝜓(𝑦). Both 𝜑 and 𝜓 may still depend on
other set variables, but that is irrelevant here.
We want to transform 𝜑(𝑥) into 𝜓(𝑦) such that 𝜓
depends on 𝑦 the same way as 𝜑 depends
on 𝑥. This
dependency is expressed in our hypothesis (called implicit
substitution): (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)). For primitive enough
𝜑 a sort of textual substitution of
𝑥
by 𝑦 is sufficient
for such transformation. But note: 𝜑 must not contain wff
variables, and the substitution is no proper textual substitution
either. We still need grammar information to not accidently replace the
x in a token 'x.' denoting multiplication, but only catch set variables
𝑥. Our current stage of development
allows only equations and
quantifiers make up such primitives. Thanks to equequ1 2047 and cbvalvw 2058
we can then prove in a mechanical way that in fact the implicit
substitution holds for each instance.
If 𝜑 contains wff variables we cannot use
textual transformation
any longer, since we don't know how to replace 𝑦 for 𝑥 in
placeholders of unknown structure. Our theorem now states, that the
generic expression ∀𝑥(𝑥 = 𝑦 → 𝜑) formally behaves as if such
a substitution was possible and made.
(Contributed by BJ, 31-May-2019.) | 