diff --git a/discouraged b/discouraged
index 6090ee15b9..695a75c5dc 100755
--- a/discouraged
+++ b/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).
diff --git a/set.mm b/set.mm
index a4a54be639..57a03ab9d5 100644
--- a/set.mm
+++ b/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