added tag and ALT version

set.mm

@@ -34695,7 +34695,8 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
     rmoanim.1 $e |- F/ x ph $.
     $( Introduction of a conjunct into restricted "at most one" quantifier,
        analogous to ~ moanim .  (Contributed by Alexander van der Vekens,
-       25-Jun-2017.) $)
+       25-Jun-2017.)  Avoid ~ ax-10 and ~ ax-11 .  (Revised by Gino Giotto,
+       24-08-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
@@ -34704,6 +34705,15 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
       KULKQUMCDRSLUGVBAUQFJZHUSVAVIAVAVDBGZCMVJULHZCNZFJVIBCDOVJCFPVLUQFVLVDUPH
       ZCNUQVKVMCVDBULKQUPCDRSLUGUHAUQFUISUJ $.
 
+    $( Alternate proof of ~ rmoanim , shorter but requiring ~ ax-10 and
+       ~ ax-11 .  (Contributed by Alexander van der Vekens, 25-Jun-2017.)
+       (New usage is discouraged.)  (Proof modification is discouraged.) $)
+    rmoanimALT $p |- ( E* x e. A ( ph /\ ps ) <-> ( ph -> E* x e. A ps ) ) $=
+      ( vy wa weq wi wral wex wrmo impexp ralbii r19.21 bitri exbii rmo2 imbi2i
+      nfv 19.37v bitr4i 3bitr4i ) ABGZCFHZIZCDJZFKABUEIZCDJZIZFKZUDCDLABCDLZIZU
+      GUJFUGAUHIZCDJUJUFUNCDABUEMNAUHCDEOPQUDCFDUDFTRUMAUIFKZIUKULUOABCFDBFTRSA
+      UIFUAUBUC $.
+
     $( Introduction of a conjunct into restricted unique existential
        quantifier, analogous to ~ euan .  (Contributed by Alexander van der
        Vekens, 2-Jul-2017.) $)