mistake correction

set.mm

@@ -45033,16 +45033,18 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
     $d x y A $.  $d y B $.  $d x C $.
     cbviunv.1 $e |- ( x = y -> B = C ) $.
     $( Rule used to change the bound variables in an indexed union, with the
-       substitution specified implicitly by the hypothesis.  See ~ cbviunv for
-       a version with more disjoint variable conditions, but not requiring
-       ~ ax-13 .  (Contributed by NM, 15-Sep-2003.) $)
+       substitution specified implicitly by the hypothesis.  (Contributed by
+       NM, 15-Sep-2003.)  Add disjoint variable condition to avoid ~ ax-13 .
+       See ~ cbviunvg for a less restrictive version requiring more axioms.
+       (Revised by Gino Giotto, 20-Jan-2024.) $)
     cbviunv $p |- U_ x e. A B = U_ y e. A C $=
       ( nfcv cbviun ) ABCDEBDGAEGFH $.
     $( $j usage 'cbviunv' avoids 'ax-13'; $)
 
-    $( Change bound variables in an indexed intersection.  See ~ cbviinv for a
-       version with more disjoint variable conditions, but not requiring
-       ~ ax-13 .  (Contributed by Jeff Hankins, 26-Aug-2009.) $)
+    $( Change bound variables in an indexed intersection.  (Contributed by Jeff
+       Hankins, 26-Aug-2009.)  Add disjoint variable condition to avoid
+       ~ ax-13 .  See ~ cbviinvg for a less restrictive version requiring more
+       axioms.  (Revised by Gino Giotto, 20-Jan-2024.) $)
     cbviinv $p |- |^|_ x e. A B = |^|_ y e. A C $=
       ( nfcv cbviin ) ABCDEBDGAEGFH $.
     $( $j usage 'cbviinv' avoids 'ax-13'; $)