I've generally gone with el* in my mathbox (see, eg., elno). I've seen is* around, but I feel el* has better compatibility with el*ab*.
On Thu, Dec 2, 2021 at 2:23 PM Benoit <[email protected]> wrote: > Many theorems in set.mm are characterizations of elements of a defined > class. For instance: ~isgrp , ~ istopg . More precisely, if we have a > definition > df-xxx $a |- Class = { x | Phi } $. > Then there is typically in set.mm a theorem isxxx. If Phi(A) does not > imply that A is a set, then there are two possible forms: > isxxx1 $p |- ( A e. Class <-> ( A e. _V /\ Phi(A) ) ) > isxxx2 $p |- ( A e. V -> ( A e. Class <-> Phi(A) ) ) > It is easy to go back and forth (using biadan2 and baib). > Is there a preferred form ? Is it ok to have both in set.mm ? It seems > to me that isxxx1 is closer to a real characterization (while isxxx2 is a > characterization among sets), but after a quick look, it seems that isxxx2 > is often (majoritarily?) used in set.mm, for instance by looking at the > number of usages of elab2g versus elab4g. > > 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/f8248f4c-ea12-4b44-b6e7-dee1e5db3feen%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/f8248f4c-ea12-4b44-b6e7-dee1e5db3feen%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CACKrHR-W6hj6nak%2BhBWzBw5u3pKG9pX7GZYTpsL4131HWJ4rtA%40mail.gmail.com.
