misc + iota axiom saves (metamath#4492)

* update sn-el and sn-dtru to use ax-pr

matches recent changes to ~ el and ~ dtru

* Replace ss2rab with ss2rabi and ss2rabdv

rgenw + ss2rab + mpbir = a1i + ss2rabi
ralrimivw + ss2rab + sylibr = adantr + ss2rabdv

Ideally ss2rabi and ss2rabdv would be renamed with an "a" suffix,
then new ss2rabi and ss2rabdv would be made.

For now it is implemented manually but it is equivalent to an
automatic shortening.

mptexgf: a1i + ss2rabi
scottex: adantr + ss2rabdv
wwlksnfi: a1i + ss2rabi
disjxwwlkn: a1i + ss2rabi
occon: adantr + ss2rabdv
rmxyelqirr: (more extensive)
itgoss: adantr + ss2rabdv
ovnsslelem: adantr + ss2rabdv (+auto minimize)
ovolval5lem3: a1i + ss2rabi (+auto minimize)

----
Add ss2ab1 and ss2abdv to mathbox, shorten abssdv

* shorten cnvsym, relssdmrn, tz6.12-1*; restore dfopifOLD

dfopifOLD no longer uses ax-10 to 12 so it is restored

* move iota axioms saves to main (rebased)

rebase: changes-set.txt, iotauni2 now uses unisnv

* add axiom file

* axiom diff (rebased, updated)

* rmv axiom file

* implement suggestions

changes-set.txt

@@ -93,6 +93,12 @@ make a github issue.)
 DONE:
 Date      Old       New         Notes
 26-Dec-24 syl5bb    bitrid      compare to bitri or bitrd
+23-Dec-24 sn-iotaex iotaex      moved from SN's mathbox to main set.mm
+23-Dec-24 sn-iotassuni iotassuni moved from SN's mathbox to main set.mm
+23-Dec-24 sn-iotaval iotaval    moved from SN's mathbox to main set.mm
+23-Dec-24 sn-iotanul iotanul2   moved from SN's mathbox to main set.mm
+23-Dec-24 sn-iotauni iotauni2   moved from SN's mathbox to main set.mm
+23-Dec-24 iotavallem iotaval2   moved from SN's mathbox to main set.mm
 19-Dec-24 3albii    [same]      moved from PM's mathbox to main set.mm
 19-Dec-24 ssrel3    [same]      moved from PM's mathbox to main set.mm
 17-Dec-24 ffvelrnd  ffvelcdmd

discouraged

@@ -14431,6 +14431,7 @@ New usage of "abn0OLD" is discouraged (0 uses).
 New usage of "abrexexgOLD" is discouraged (0 uses).
 New usage of "abscncfALT" is discouraged (0 uses).
 New usage of "abshicom" is discouraged (1 uses).
+New usage of "abssdvOLD" is discouraged (0 uses).
 New usage of "abvALT" is discouraged (0 uses).
 New usage of "ac2" is discouraged (1 uses).
 New usage of "ac3" is discouraged (1 uses).
@@ -15782,6 +15783,7 @@ New usage of "cnvbramul" is discouraged (1 uses).
 New usage of "cnvbraval" is discouraged (1 uses).
 New usage of "cnvfiALT" is discouraged (0 uses).
 New usage of "cnvoprabOLD" is discouraged (0 uses).
+New usage of "cnvsymOLD" is discouraged (0 uses).
 New usage of "cnvunop" is discouraged (2 uses).
 New usage of "com3rgbi" is discouraged (1 uses).
 New usage of "con3ALT" is discouraged (0 uses).
@@ -16047,7 +16049,6 @@ New usage of "dfmo" is discouraged (0 uses).
 New usage of "dfnul2OLD" is discouraged (0 uses).
 New usage of "dfnul3OLD" is discouraged (0 uses).
 New usage of "dfnul4OLD" is discouraged (0 uses).
-New usage of "dfopifOLD" is discouraged (0 uses).
 New usage of "dfpjop" is discouraged (4 uses).
 New usage of "dfrecs3OLD" is discouraged (0 uses).
 New usage of "dfsb1" is discouraged (4 uses).
@@ -17353,6 +17354,9 @@ New usage of "intprOLD" is discouraged (0 uses).
 New usage of "intprgOLD" is discouraged (0 uses).
 New usage of "iorlid" is discouraged (2 uses).
 New usage of "iotaeq" is discouraged (0 uses).
+New usage of "iotaexOLD" is discouraged (0 uses).
+New usage of "iotassuniOLD" is discouraged (0 uses).
+New usage of "iotavalOLD" is discouraged (0 uses).
 New usage of "ip0i" is discouraged (1 uses).
 New usage of "ip1i" is discouraged (2 uses).
 New usage of "ip1ilem" is discouraged (1 uses).
@@ -18794,6 +18798,7 @@ New usage of "relop" is discouraged (1 uses).
 New usage of "relopabVD" is discouraged (0 uses).
 New usage of "relopabiALT" is discouraged (0 uses).
 New usage of "relrngo" is discouraged (6 uses).
+New usage of "relssdmrnOLD" is discouraged (0 uses).
 New usage of "renegclALT" is discouraged (0 uses).
 New usage of "renicax" is discouraged (0 uses).
 New usage of "rescabsOLD" is discouraged (0 uses).
@@ -18859,6 +18864,7 @@ New usage of "rlimmulOLD" is discouraged (0 uses).
 New usage of "rmoanimALT" is discouraged (0 uses).
 New usage of "rmobidvaOLD" is discouraged (0 uses).
 New usage of "rmodislmodOLD" is discouraged (0 uses).
+New usage of "rmxyelqirrOLD" is discouraged (0 uses).
 New usage of "rnbra" is discouraged (2 uses).
 New usage of "rnelshi" is discouraged (1 uses).
 New usage of "rngcbasALTV" is discouraged (6 uses).
@@ -19128,6 +19134,7 @@ New usage of "smfval" is discouraged (17 uses).
 New usage of "smgrpassOLD" is discouraged (1 uses).
 New usage of "smgrpismgmOLD" is discouraged (1 uses).
 New usage of "smgrpmgm" is discouraged (1 uses).
+New usage of "sn-elALT2" is discouraged (0 uses).
 New usage of "sn-wcdeq" is discouraged (0 uses).
 New usage of "snatpsubN" is discouraged (3 uses).
 New usage of "snelpwrVD" is discouraged (0 uses).
@@ -19379,6 +19386,8 @@ New usage of "ttgplusgOLD" is discouraged (0 uses).
 New usage of "ttgvalOLD" is discouraged (0 uses).
 New usage of "ttgvscaOLD" is discouraged (0 uses).
 New usage of "tuslemOLD" is discouraged (0 uses).
+New usage of "tz6.12-1OLD" is discouraged (0 uses).
+New usage of "tz6.12cOLD" is discouraged (0 uses).
 New usage of "tz6.26OLD" is discouraged (0 uses).
 New usage of "ubth" is discouraged (1 uses).
 New usage of "ubthlem1" is discouraged (1 uses).
@@ -19682,6 +19691,7 @@ Proof modification of "abfOLD" is discouraged (13 steps).
 Proof modification of "abn0OLD" is discouraged (28 steps).
 Proof modification of "abrexexgOLD" is discouraged (43 steps).
 Proof modification of "abscncfALT" is discouraged (71 steps).
+Proof modification of "abssdvOLD" is discouraged (24 steps).
 Proof modification of "abvALT" is discouraged (36 steps).
 Proof modification of "ackm" is discouraged (71 steps).
 Proof modification of "addltmulALT" is discouraged (497 steps).
@@ -20102,6 +20112,7 @@ Proof modification of "cnncvsaddassdemo" is discouraged (46 steps).
 Proof modification of "cnncvsmulassdemo" is discouraged (95 steps).
 Proof modification of "cnvfiALT" is discouraged (46 steps).
 Proof modification of "cnvoprabOLD" is discouraged (262 steps).
+Proof modification of "cnvsymOLD" is discouraged (88 steps).
 Proof modification of "com3rgbi" is discouraged (35 steps).
 Proof modification of "con3ALT" is discouraged (54 steps).
 Proof modification of "con3ALT2" is discouraged (14 steps).
@@ -20150,7 +20161,6 @@ Proof modification of "dfmo" is discouraged (44 steps).
 Proof modification of "dfnul2OLD" is discouraged (38 steps).
 Proof modification of "dfnul3OLD" is discouraged (42 steps).
 Proof modification of "dfnul4OLD" is discouraged (23 steps).
-Proof modification of "dfopifOLD" is discouraged (102 steps).
 Proof modification of "dfrecs3OLD" is discouraged (263 steps).
 Proof modification of "dfsn2ALT" is discouraged (30 steps).
 Proof modification of "dfss2OLD" is discouraged (56 steps).
@@ -20778,6 +20788,9 @@ Proof modification of "int2" is discouraged (14 steps).
 Proof modification of "int3" is discouraged (17 steps).
 Proof modification of "intprOLD" is discouraged (112 steps).
 Proof modification of "intprgOLD" is discouraged (80 steps).
+Proof modification of "iotaexOLD" is discouraged (57 steps).
+Proof modification of "iotassuniOLD" is discouraged (35 steps).
+Proof modification of "iotavalOLD" is discouraged (101 steps).
 Proof modification of "isarep1OLD" is discouraged (106 steps).
 Proof modification of "iscmgmALT" is discouraged (57 steps).
 Proof modification of "iscsgrpALT" is discouraged (57 steps).
@@ -21148,6 +21161,7 @@ Proof modification of "refsymrels3" is discouraged (56 steps).
 Proof modification of "reldisjOLD" is discouraged (86 steps).
 Proof modification of "relopabVD" is discouraged (354 steps).
 Proof modification of "relopabiALT" is discouraged (74 steps).
+Proof modification of "relssdmrnOLD" is discouraged (75 steps).
 Proof modification of "renegcl" is discouraged (34 steps).
 Proof modification of "renegclALT" is discouraged (149 steps).
 Proof modification of "renicax" is discouraged (76 steps).
@@ -21187,6 +21201,7 @@ Proof modification of "rlimmulOLD" is discouraged (159 steps).
 Proof modification of "rmoanimALT" is discouraged (93 steps).
 Proof modification of "rmobidvaOLD" is discouraged (10 steps).
 Proof modification of "rmodislmodOLD" is discouraged (1641 steps).
+Proof modification of "rmxyelqirrOLD" is discouraged (238 steps).
 Proof modification of "rngopidOLD" is discouraged (27 steps).
 Proof modification of "rnmptcOLD" is discouraged (54 steps).
 Proof modification of "rntrclfv" is discouraged (46 steps).
@@ -21271,6 +21286,7 @@ Proof modification of "slotsbhcdifOLD" is discouraged (96 steps).
 Proof modification of "smgrpassOLD" is discouraged (54 steps).
 Proof modification of "smgrpismgmOLD" is discouraged (22 steps).
 Proof modification of "sn-00id" is discouraged (50 steps).
+Proof modification of "sn-elALT2" is discouraged (52 steps).
 Proof modification of "snelpwrVD" is discouraged (37 steps).
 Proof modification of "snex" is discouraged (64 steps).
 Proof modification of "snexALT" is discouraged (48 steps).
@@ -21393,6 +21409,8 @@ Proof modification of "ttgplusgOLD" is discouraged (25 steps).
 Proof modification of "ttgvalOLD" is discouraged (845 steps).
 Proof modification of "ttgvscaOLD" is discouraged (25 steps).
 Proof modification of "tuslemOLD" is discouraged (304 steps).
+Proof modification of "tz6.12-1OLD" is discouraged (30 steps).
+Proof modification of "tz6.12cOLD" is discouraged (60 steps).
 Proof modification of "tz6.26OLD" is discouraged (96 steps).
 Proof modification of "umgr2adedgwlkonALT" is discouraged (294 steps).
 Proof modification of "un0.1" is discouraged (21 steps).