move eqneltri to other eqnel* theorems (#4662)

set.mm

@@ -26225,15 +26225,6 @@ the definition of class equality ( ~ df-cleq ).  Its forward implication
     $}
   $}
 
-  ${
-    eqneltri.1 $e |- A = B $.
-    eqneltri.2 $e |- -. B e. C $.
-    $( If a class is not an element of another class, an equal class is also
-       not an element.  (Contributed by Glauco Siliprandi, 3-Jan-2021.) $)
-    eqneltri $p |- -. A e. C $=
-      ( wcel eleq1i mtbir ) ACFBCFEABCDGH $.
-  $}
-
   ${
     eleq12d.1 $e |- ( ph -> A = B ) $.
     eleq12d.2 $e |- ( ph -> C = D ) $.
@@ -26463,6 +26454,15 @@ the definition of class equality ( ~ df-cleq ).  Its forward implication
       ( wcel eleq2i sylbi ) BDGBCGADCBFHEI $.
   $}
 
+  ${
+    eqneltri.1 $e |- A = B $.
+    eqneltri.2 $e |- -. B e. C $.
+    $( If a class is not an element of another class, an equal class is also
+       not an element.  (Contributed by Glauco Siliprandi, 3-Jan-2021.) $)
+    eqneltri $p |- -. A e. C $=
+      ( wcel eleq1i mtbir ) ACFBCFEABCDGH $.
+  $}
+
   ${
     eqneltrd.1 $e |- ( ph -> A = B ) $.
     eqneltrd.2 $e |- ( ph -> -. B e. C ) $.