Description: Version of equsalv with a disjoint variable condition, and of equsal with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsexvw .
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 ph and y disjoint, stated here as ph ( x ) . Similarly the disjointness of ps and x is expressed by ps ( y ) . Both ph and ps may still depend on other set variables, but that is irrelevant here.
We want to transform ph ( x ) into ps ( y ) such that ps depends on y the same way as ph depends on x . This dependency is expressed in our hypothesis (called implicit substitution): ( x = y -> ( ph <-> ps ) ) . For primitive enough ph a sort of textual substitution of x by y is sufficient for such transformation. But note: ph 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 x . Our current stage of development allows only equations and quantifiers make up such primitives. Thanks to equequ1 and cbvalvw we can then prove in a mechanical way that in fact the implicit substitution holds for each instance.
If ph contains wff variables we cannot use textual transformation any longer, since we don't know how to replace y for x in placeholders of unknown structure. Our theorem now states, that the generic expression A. x ( x = y -> ph ) formally behaves as if such a substitution was possible and made.
(Contributed by BJ, 31-May-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | wl-equsalvw.1 | |- ( x = y -> ( ph <-> ps ) ) |
|
| Assertion | wl-equsalvw | |- ( A. x ( x = y -> ph ) <-> ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wl-equsalvw.1 | |- ( x = y -> ( ph <-> ps ) ) |
|
| 2 | 19.23v | |- ( A. x ( x = y -> ps ) <-> ( E. x x = y -> ps ) ) |
|
| 3 | 1 | pm5.74i | |- ( ( x = y -> ph ) <-> ( x = y -> ps ) ) |
| 4 | 3 | albii | |- ( A. x ( x = y -> ph ) <-> A. x ( x = y -> ps ) ) |
| 5 | ax6ev | |- E. x x = y |
|
| 6 | 5 | a1bi | |- ( ps <-> ( E. x x = y -> ps ) ) |
| 7 | 2 4 6 | 3bitr4i | |- ( A. x ( x = y -> ph ) <-> ps ) |