rename mofsn3 -> mofmo; and fix description

set.mm

@@ -775875,9 +775875,9 @@ additional condition (deduction form).  See ~ ralbidc for a more
       ZUJUKKUNAUIULJZCTZUKUPUJADCGLMUJUNUPNUKUJUMUOCBUIAULOPQRUJUKUAZKZBSFUNURB
       UISUJUQUBUQUISFZUJUQUSDUCUDMUEABCUFUGUH $.
 
-    $( At most one function to a implied singleton. ~ mofsn .  (Contributed by
-       Zhi Wang, 19-Sep-2024.) $)
-    mofsn3 $p |- ( E* x x e. B -> E* f f : A --> B ) $=
+    $( At most one function to a class containing at most one element.
+       (Contributed by Zhi Wang, 19-Sep-2024.) $)
+    mofmo $p |- ( E* x x e. B -> E* f f : A --> B ) $=
       ( vy cv wcel wmo c0 wceq csn wex wo mo0sn mof02 mofsn2 exlimiv jaoi sylbi
       wf ) AFCGAHCIJZCEFZKJZELZMBCDFTDHZAECNUAUEUDBCDOUCUEEBCDUBPQRS $.
   $}
@@ -777365,11 +777365,11 @@ separated by (open) neighborhoods.  See ~ sepnsepo for the equivalence
        (Contributed by Zhi Wang, 20-Sep-2024.) $)
     setcthin $p |- ( ph -> C e. ThinCat ) $=
       ( vy vz vf cfv eqid cv wcel wa wmo mobidv adantr csetc chom setcbas eqidd
-      cthinc co wf weq elequ2 simprr rspcdva mofsn3 syl simprl elsetchom mpbird
-      wral ccat setccat isthincd eqeltrd ) ACDUAMZUEGAJKDVBLVBUBMZAVBDEVBNZHUCA
-      VCUDAJOZDPZKOZDPZQZQZLOZVEVGVCUFPZLRVEVGVKUGZLRZVJFOZVGPZFRZVNVJVOBOPZFRZ
-      VQBDVGBKUHVRVPFBKFUISAVSBDUQVIITAVFVHUJZUKFVEVGLULUMVJVLVMLVJVBDVKVCEVEVG
-      VDADEPZVIHTVCNAVFVHUNVTUOSUPAWAVBURPHVBDEVDUSUMUTVA $.
+      cthinc co wf weq elequ2 wral simprr rspcdva mofmo simprl elsetchom mpbird
+      syl ccat setccat isthincd eqeltrd ) ACDUAMZUEGAJKDVBLVBUBMZAVBDEVBNZHUCAV
+      CUDAJOZDPZKOZDPZQZQZLOZVEVGVCUFPZLRVEVGVKUGZLRZVJFOZVGPZFRZVNVJVOBOPZFRZV
+      QBDVGBKUHVRVPFBKFUISAVSBDUJVIITAVFVHUKZULFVEVGLUMUQVJVLVMLVJVBDVKVCEVEVGV
+      DADEPZVIHTVCNAVFVHUNVTUOSUPAWAVBURPHVBDEVDUSUQUTVA $.
   $}
 
   ${