On Sunday, June 2, 2019 at 12:52:21 PM UTC-4, Tony wrote: > > On Sunday, June 2, 2019 at 6:02:30 PM UTC+2, Norman Megill wrote: > > We have been calling [. A / x ]. ph "explicit" (because it has an explicit >> substitution symbol) and "x = A -> ( ph <-> ps )" "implicit". See the >> descriptions of ~ sbie and ~ sbcie. >> > > I have no idea what "implicit substitution" means. I don't understand what > any of the theorems containing constructions like x = A -> ( ph <-> ps ) > is about. >
Compare the explicit substitution version of finite induction (on ordinals) http://us.metamath.org/mpeuni/findes.html with the implicit substitution version http://us.metamath.org/mpeuni/finds.html Note that the implicit version has found more uses, although that may be partly because the implicit version has an additional hypothesis to give us a more useful class variable rather than a setvar variable in the conclusion. Norm -- 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/2fff7c5f-4c2f-46f0-bd5a-67ccbb25db0a%40googlegroups.com.
