move nax6im back to mathbox

set.mm

@@ -15582,26 +15582,6 @@ only postulated (that is, axiomatic) rule of inference of predicate
   so are also every universal quantification of ~ ax-7 , ~ ax-8 and ~ ax-9 .
 $)
 
-  ${
-    $d x y $.
-    nax6im.1 $e |- ( -. E. x x = y -> ph ) $.
-    $( The following series of theorems are centered around the empty domain,
-       where no set exists.  As a consequence, a set variable like ` x ` has no
-       instance to assign to.  An expression like ` x = y ` is not really
-       meaningful then.  What does it evaluate to, true or false?  In fact, the
-       grammar extension ~ weq requires us to formally assign a boolean value
-       to an equation, say always false, unless you want to give up on
-       ~ exmid , for example.  Whatever it is, we start out with the
-       contraposition of ~ ax-6 , that guarantees the existence of at least one
-       set.  Our hypothesis here expresses tentatively it might not hold.  We
-       can simplify the antecedent then, to the point where we do not need
-       equation any more.  This suggests what a decent characterization of the
-       empty logical domain could be.  (Contributed by Wolf Lammen,
-       12-Mar-2023.) $)
-    nax6im $p |- ( -. E. x T. -> ph ) $=
-      ( wtru wex weq trud eximi nsyl4 con1i ) AEBFZBCGZBFLAMEBMHIDJK $.
-  $}
-
   $( In an empty logical domain existential quantification never holds, not
      even for false expressions.  (Contributed by Wolf Lammen, 21-Jan-2024.) $)
   nax6ex $p |- ( -. E. x T. -> -. E. x ph ) $=
@@ -541355,6 +541335,26 @@ extends this idea to multiple additions (TODO).
       AEZCAFZGPABHAICAJOPAKLABMN $.
   $}
 
+  ${
+    $d x y $.
+    wl-nax6im.1 $e |- ( -. E. x x = y -> ph ) $.
+    $( The following series of theorems are centered around the empty domain,
+       where no set exists.  As a consequence, a set variable like ` x ` has no
+       instance to assign to.  An expression like ` x = y ` is not really
+       meaningful then.  What does it evaluate to, true or false?  In fact, the
+       grammar extension ~ weq requires us to formally assign a boolean value
+       to an equation, say always false, unless you want to give up on
+       ~ exmid , for example.  Whatever it is, we start out with the
+       contraposition of ~ ax-6 , that guarantees the existence of at least one
+       set.  Our hypothesis here expresses tentatively it might not hold.  We
+       can simplify the antecedent then, to the point where we do not need
+       equation any more.  This suggests what a decent characterization of the
+       empty logical domain could be.  (Contributed by Wolf Lammen,
+       12-Mar-2023.) $)
+    wl-nax6im $p |- ( -. E. x T. -> ph ) $=
+      ( wtru wex weq trud eximi nsyl4 con1i ) AEBFZBCGZBFLAMEBMHIDJK $.
+  $}
+
   $( This specialization of ~ hbae does not depend on ~ ax-11 .  (Contributed
      by Wolf Lammen, 8-Aug-2021.) $)
   wl-hbae1 $p |- ( A. x x = y -> A. y A. x x = y ) $=