Users' Mathboxes Mathbox for Wolf Lammen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wl-equsalvw Structured version   Visualization version   GIF version

Theorem wl-equsalvw 34310
Description: Version of equsalv 2231 with a disjoint variable condition, and of equsal 2395 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsexvw 1988.

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 2009 and cbvalvw 2020 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.)

Ref Expression
wl-equsalvw.1 (𝑥 = 𝑦 → (𝜑𝜓))
Ref Expression
wl-equsalvw (∀𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
Distinct variable groups:   𝑥,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)

Proof of Theorem wl-equsalvw
StepHypRef Expression
1 19.23v 1920 . 2 (∀𝑥(𝑥 = 𝑦𝜓) ↔ (∃𝑥 𝑥 = 𝑦𝜓))
2 wl-equsalvw.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32pm5.74i 272 . . 3 ((𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑦𝜓))
43albii 1801 . 2 (∀𝑥(𝑥 = 𝑦𝜑) ↔ ∀𝑥(𝑥 = 𝑦𝜓))
5 ax6ev 1949 . . 3 𝑥 𝑥 = 𝑦
65a1bi 364 . 2 (𝜓 ↔ (∃𝑥 𝑥 = 𝑦𝜓))
71, 4, 63bitr4i 304 1 (∀𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1520  wex 1761
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947
This theorem depends on definitions:  df-bi 208  df-ex 1762
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator