fixes

discouraged

@@ -17446,6 +17446,7 @@ New usage of "ringcsectALTV" is discouraged (1 uses).
 New usage of "ringcvalALTV" is discouraged (3 uses).
 New usage of "riotaocN" is discouraged (1 uses).
 New usage of "rmo3OLD" is discouraged (0 uses).
+New usage of "rmoanimALT" is discouraged (0 uses).
 New usage of "rmoeq1OLD" is discouraged (0 uses).
 New usage of "rnbra" is discouraged (2 uses).
 New usage of "rnelshi" is discouraged (1 uses).
@@ -19601,6 +19602,7 @@ Proof modification of "rexsngOLD" is discouraged (25 steps).
 Proof modification of "rgen2a" is discouraged (81 steps).
 Proof modification of "rim0to0OLD" is discouraged (92 steps).
 Proof modification of "rmo3OLD" is discouraged (179 steps).
+Proof modification of "rmoanimALT" is discouraged (93 steps).
 Proof modification of "rmoeq1OLD" is discouraged (11 steps).
 Proof modification of "rngopidOLD" is discouraged (27 steps).
 Proof modification of "rntrclfv" is discouraged (46 steps).

set.mm

@@ -34696,7 +34696,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
     $( Introduction of a conjunct into restricted "at most one" quantifier,
        analogous to ~ moanim .  (Contributed by Alexander van der Vekens,
        25-Jun-2017.)  Avoid ~ ax-10 and ~ ax-11 .  (Revised by Gino Giotto,
-       24-08-2023.) $)
+       24-Aug-2023.) $)
     rmoanim $p |- ( E* x e. A ( ph /\ ps ) <-> ( ph -> E* x e. A ps ) ) $=
       ( vy wa wi wral wex impexp exbii wmo wal df-rmo df-mo albii df-ral bitr4i
       wrmo weq ralbii r19.21 bitri cv wcel 3bitri imbi2i 19.37v 3bitr4i ) ABGZC