From a36d0f3f98359dfe6ba7931ff21ef2e22e7fb111 Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Mon, 30 Sep 2024 14:28:09 +0200
Subject: [PATCH] move ralidmw

---
 set.mm | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/set.mm b/set.mm
index 07957546e4..6c0e2fdb9f 100644
--- a/set.mm
+++ b/set.mm
@@ -41202,6 +41202,20 @@ disjoint classes (see ~ disjdif ).  Part of proof of Corollary 6K of
       HZGOBGABCDJNBPOBCDKLM $.
   $}
 
+  ${
+    $d x y A $.  $d ph y $.  $d ps x $.
+    ralidmw.1 $e |- ( x = y -> ( ph <-> ps ) ) $.
+    $( Idempotent law for restricted quantifier.  Weak version of ~ ralidm ,
+       which does not require ~ ax-10 , ~ ax-12 , but requires ~ ax-8 .
+       (Contributed by Gino Giotto, 30-Sep-2024.) $)
+    ralidmw $p |- ( A. x e. A A. x e. A ph <-> A. x e. A ph ) $=
+      ( cv wcel wral wi wal df-ral imbi2i albii pm2.21 weq eleq1w imbi12d spw
+      ja alimi hba1w ax-1 alrimih impbii bitri 3bitr4i ) CGEHZACEIZJZCKZUHAJZCK
+      ZUICEIUIUKUHUMJZCKZUMUJUNCUIUMUHACELZMNUOUMUNULCUHUMULUHAOULDGEHZBJZCDCDP
+      UHUQABCDEQFRZSTUAUMUNCULURCDUSUBUMUHUCUDUEUFUICELUPUG $.
+    $( $j usage 'ralidmw' avoids 'ax-10' 'ax-11' 'ax-12'; $)
+  $}
+
   ${
     $d x A $.  $d x y $.
     $( Vacuous quantification is always true.  (Contributed by NM,
@@ -41230,20 +41244,6 @@ disjoint classes (see ~ disjdif ).  Part of proof of Corollary 6K of
       EHZFABCIQPOBCJKLM $.
     $( $j usage 'rexn0' avoids 'df-clel' 'ax-8'; $)
 
-    ${
-      $d ph y $.  $d ps x $.  $d x y $.  $d A y $.
-      ralidmw.1 $e |- ( x = y -> ( ph <-> ps ) ) $.
-      $( Idempotent law for restricted quantifier.  Version of ~ ralidm using
-         implicit substitution, which does not require ~ ax-10 , ~ ax-12 , but
-         requires ~ ax-8 .  (Contributed by Gino Giotto, 30-Sep-2024.) $)
-      ralidmw $p |- ( A. x e. A A. x e. A ph <-> A. x e. A ph ) $=
-        ( cv wcel wral wi wal df-ral imbi2i albii pm2.21 weq eleq1w imbi12d spw
-        ja alimi hba1w ax-1 alrimih impbii bitri 3bitr4i ) CGEHZACEIZJZCKZUHAJZ
-        CKZUICEIUIUKUHUMJZCKZUMUJUNCUIUMUHACELZMNUOUMUNULCUHUMULUHAOULDGEHZBJZC
-        DCDPUHUQABCDEQFRZSTUAUMUNCULURCDUSUBUMUHUCUDUEUFUICELUPUG $.
-      $( $j usage 'ralidmw' avoids 'ax-10' 'ax-11' 'ax-12'; $)
-    $}
-
     $( Idempotent law for restricted quantifier.  (Contributed by NM,
        28-Mar-1997.)  Reduce axiom usage.  (Revised by Gino Giotto,
        2-Sep-2024.) $)