Hi, Il 02/06/19 13:37, Tony ha scritto: > Thank you! I couldn't find those by myself.
They use class substitution (i.e., [. ].) instead of set substitution (i.e., [ ]). My understanding is that class substitution is the one that should be used in "higher-level" proof, with set substitution just being used in turn to properly support class substitution. The "end-user" theorems are probably easier to find for class substitution (although, of course, in the end what you are going to substitute is a set anyway, but not necessarily a set variable). > Is using those theorems the best way to do substitution? Seems like > there can be a lot of steps for something you would normally do in a > single step in an informal proof. I guess this is one of the prices you pay for having formal proofs (and for having such a low level language like Metamath): you have to deal with really boring and, to the extent one is normally used to, trivial details. Ideally it would be nice to have some more help from tooling here, and it is one of the things I am working on with my project mmpp (but it is not yet ready). This is BTW the reason why I knew the answer to your question immediately! I also have variants of sbcan and a few others in inference form in my mathbox: http://us2.metamath.org/mpeuni/mmtheorems284.html#sbcani With these variants you directly construct the substitution of a complex formula without having to use a lot of mp* or syl* at each depth stage. Giovanni. -- Giovanni Mascellani <[email protected]> Postdoc researcher - Université Libre de Bruxelles -- 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/735b549b-1ff5-fb17-512d-a48f840e224e%40gmail.com.
signature.asc
Description: OpenPGP digital signature
