Move ifexd to Main.

[benjub]

• Minor shortening of iset/cnstab.
• Move ifexd to Main and minimize ifexg with it, as announced in https://github.com/metamath/set.mm/pull/4130#discussion_r1719654644

[avekens]

* Move ifexd to Main and minimize ifexg with it, as announced in [illustrate "Projective spaces" section header #4130 (comment)](https://github.com/metamath/set.mm/pull/4130#discussion_r1719654644)

Are ther other prrof which can be shortened using ifexd?

[benjub]

Ups, I forgot something: the movement should be documented in changes-set.txt

It's in the commit message, which is what matters for tracking history. It's not breaking anything in Main, so no need to edit the changes file.

[avekens]

Ups, I forgot something: the movement should be documented in changes-set.txt

It's in the commit message, which is what matters for tracking history. It's not breaking anything in Main, so no need to edit the changes file.

It is an established practice for a long time that theorems which were moved from (at least other's) maxboxes to main are documented in changes-set.txt (see, for example, https://groups.google.com/g/metamath/c/dGW5v81srRY/m/-u_Qq1YCAwAJ in the Google group). I do not know the exact reason for it (anymore), but I think it was to give a hint for the mathbox owner why a theorem seems to be missing in his mathbox. Looking up the git history for such changes is very tedious, escpecially because we have a single file set.mm with an enormous amount of changes.

Unfortunately, this seems not to be documented anywhere (neither in changes-set.txt itself nor in set.mm - here we only have "For a chronological list of changes to label names and label deletions, see the changes-set.txt file. This should help if you have a proof not checked into the main repository and want to update it for recent changes").

[icecream17]

since I know that it was moved I'm indifferent to this change

[avekens]

This rule is also mentioned in the proposed "Contribution principles" by @jkingdon , see issue #3483.

[jkingdon]

It is an established practice for a long time that theorems which were moved from (at least other's) maxboxes to main are documented in changes-set.txt

Yeah, I've just taken it for granted that this happens. I don't really know if there has been a lot of discussion on it (I don't remember any).

[benjub]

So... we're just following a rule because it's a rule even though we do not know why it exists ?

[tirix]

So... we're just following a rule because it's a rule even though we do not know why it exists ?

I think the rule is really useful for renames like syl6bbr to bitr4di. It's also useful when a theorem is renamed at the same time as it is moved to main. In both cases, in order to adapt pending changes to the changes already in the develop branch.

Other than that, I find it entertaining and interesting to see which theorems are moved to main (e.g. there is a big recent trend to move deduction variants), but I don't think it's absolutely necessary.

The table and the rule must have originated from the time when Git was not used yet and there was no change tracking. Git makes it less useful for sure.