On Sun, May 8, 2022 at 3:02 PM 'Alexander van der Vekens' via Metamath
> (...) 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.) ?