Stan: you're right about the need to prove this (if using explicit substitution): look for the utility theorems exchanging [. / ]. with other symbols (quantifiers, operations). As said by Jim and Thierry, who are more experienced in proof building, implicit substitution might be easier to use. I think it is instructive to compare the details of both proving styles on a specific example (e.g. ralbidv, suggested by Thierry, would be analogous to exchanging [. / ]. with A.).
Still, I think adding what I called rspesbcd could prove useful (if it is not already in set.mm under another label; I cannot search now, but it probably is already somewhere). Benoît -- 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/ebdd296f-6bcd-49e0-88c8-c7fef3628cdd%40googlegroups.com.
