On Tue, May 28, 2019 at 3:25 PM Giovanni Mascellani <[email protected]> wrote:
> Hi! I think there is a general trick to replace a $d x A or $d x ph$ > condition in a theorem with the corresponding F/_ x A or F/ x ph, but I > do not remember it. Can anybody help me? > The technique is the following. Suppose you have |- T[x, A] where $d x A, and you wish to prove |- F/_ x A => |- T[x, A]. You apply the theorem substituting y for x and A for A, where y is a new dummy variable, so that $d y A is satisfied. You obtain |- T[y, A], and apply chvar to obtain |- T[x, A] (or just use mpbir if T[x, A] binds x). The side goal is |- ( x = y -> ( T[y, A] <-> T[x, A] ) ), where you can use equality theorems, except that when you get to a bound variable you use a non-dv bound variable renamer theorem like cbval. The section us2.metamath.org/mpeuni/mmtheorems32.html#mm3146s also describes the metatheorem that underlies this. > PS. I already asked the same question on the Metamath Gitter channel[1], > but I believe it is not very active at the moment! > > [1] https://gitter.im/metamath/Lobby As you probably noticed, the gitter lobby gets one post a year or so. I thought it might be helpful for people who like the chat style, but gitter doesn't notify me when something comes in so given the tiny traffic it's pretty hard to get a quick response, and your post might just sit there for months before someone notices. The google group is definitely the best way to get attention from the metamath community right now. Mario -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSt3T4EyNGXNhg2M2pdEBzzr5L_BvksSC_AAk9L%2BAbhuzw%40mail.gmail.com.
