Fix a $j-comment.

metamath · Jan 12, 2025 · 558d7b5 · 558d7b5
1 parent 7884aba
commit 558d7b5
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/set.mm b/set.mm
@@ -93797,7 +93797,7 @@ singletons being the empty set ( ` A e/ _V ` ).  (Contributed by AV,
   1sdom2ALT $p |- 1o ~< 2o $=
     ( c1o csuc c2o csdm com wcel wbr 1onn php4 ax-mp df-2o breqtrri ) AABZCDAEF
     AMDGHAIJKL $.
-  $( $j usage '1sdom2' avoids 'ax-pow'; $)
+  $( $j usage '1sdom2ALT' avoids 'ax-pow'; $)
 
   ${
     $d A x $.  $d A f $.