Follow up of # 4648

[wlammen]

In #4648 some issues weren't resolved. This PR adds the missing points.

1. The variant abeq2 seems to be the basic block from which most variants covered here are derived. A new name abeqb was suggested, but the sequence abeq has a different meaning in rabeq, and clashes are the consequence. Instead I used the left hand side 𝐴 = {𝑥 ∣ 𝜑} as the name building item and decided to rename this theorem to eqab (short for equals a class abstraction) still close to the old name, but unused in set.mm so far.
2. Theorem abeq1 is renamed to eqabc, the suffix c usually standing for a commuted form.
3. abeq2impr is now eqab1r. The suffix 1 indicates a less expressive variant (implication instead of bi-directional), and the r is short for reverse direction). This naming pattern follows that of abbi1. This theorem is located before eqab, as requested by commenters in prove one direction of abeq2 from fewer axioms #4648 . A missing $j tag is now added.
4. All other renamings follow these examples abeq2 -> eqab resp. abeq1 -> eqabc suit
5. nf.mm and some other files need this renaming, too. Otherwise check in failures are the result. Hopefully I got everything right.

I suggest to look through this PR commit by commit for easier review.

[benjub]

I like the renamings to eqab and the suffix c for the commuted forms. However, for reverse implication, can you use the suffix ri to follow common usage ? This entails the relabeling:

`eqab1r` --> eqabri

[wlammen]

How would you name a theorem that uses the forward implication then? It clashes with eqabi, the immediate version of eqab.

[benjub]

How would you name a theorem that uses the forward implication then? It clashes with eqabi, the immediate version of eqab.

I propose the label eqabri with an "r", so it does not clash with eqabi. If you mean "what if we had to add the associated inference", yes, indeed it would clash: we know we have to make concessions because of the combinatorial explosion of the number of statements and because we want to keep reasonable-length labels. If you prefer, we can label it eqabr without the "i". I think the number "1" should be avoided as not having an obvious meaning.

[avekens]

The suffix "i" is also used as "implication", see the table of label fragments in our Conventions.

By the way, the label fragment "ri" should be added to this table.

[benjub]

I agree with @wlammen and @avekens, suffix should be r only, without ì. Examples: notnotr, pm5.31r, nfcr, nf5r... So eqabr suffices.

[avekens]

I agree with @wlammen and @avekens, suffix should be r only, without ì. Examples: notnotr, pm5.31r, nfcr, nf5r... So eqabr suffices.

Our Conventions do contain this already (Bullet point "Suffixes") :

r : theorem with something reversed (e.g., a biconditional)

[icecream17]

could abeq1 be abeq instead of eqabc? Though eqabr would still be eqabr or be something like abeqim

[wlammen]

could abeq1 be abeq instead of eqabc? Though eqabr would still be eqabr or be something like abeqim

I wanted to get away from abeq, since this sequence has a different meaning in rabeq and some other theorems. I had to start over again to resolve some surprising clashes in the process of renaming. So I am for this PR against it.