On Sun, May 8, 2022 at 3:02 PM 'Alexander van der Vekens' via Metamath <[email protected]> wrote: > > (...) I would suggest to enhance the item "Theorem forms." as follows: > (...) > When an inference is converted to a theorem by eliminating an "is a > set" > hypothesis, we sometimes suffix the closed form with "g" (for "more > general") as in ~ uniex vs. ~ uniexg .
We can eliminate hundreds of inferences with "is a set" hypothesis by means of ~ elv , ~ el2v and ~ el3v , e.g. by deleting ~ uniex (Contributed by NM, 11-Aug-1993.) and renaming ~ uniexg (Contributed by NM, 25-Nov-1994.) to ~ uniex at the same time, and where you need the inference form, use |- ( x e. _V -> U. x e. _V ) and ~ elv (sometimes ~ ax-mp ). The main problem here is not mathematical: who is the contributor of the remaining theorem? (Contributed by NM, 11-Aug-1993.) (Reviewed by NM, 25-Nov-1994.) ? P. -- 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/CAJJTU5rY%3DQ7ExK9NNgrBHCEWbbwvOMeoE8TAMCL8ctMuHy4RLw%40mail.gmail.com.
