> > 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
My limited experience confirms this: sbc* theorems get more used than their sb* counterparts outside of FOL. > (although, of course, in the end what you are going to substitute is a set > anyway, > but not necessarily a set variable). I would rather think of it as: "In the end, what you are going to substitute is generally a term, not a variable"... which confirms that sbc* theorems are more useful than sb* theorems. > > 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) I think that it is often possible to avoid "[ / ]-substitutions" (are they the ones called "implicit substitutions"?) by modifying your proof a bit, and use "explicit substitution" instead (typically with steps like "x = A -> ( ph <-> ps )"). It would be interesting that someone with more practice confirms/infirms this. Benoit -- 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/d9b9323e-9b60-489a-9a23-5a3564575f3e%40googlegroups.com.
