From 749e452d69c91ee98fcd0dfb90293753b1eaf338 Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Mon, 14 Oct 2024 14:10:40 +0200
Subject: [PATCH 1/4] remove DV conditions

---
 set.mm | 156 +++++++++++++++++++++++++++++++--------------------------
 1 file changed, 84 insertions(+), 72 deletions(-)

diff --git a/set.mm b/set.mm
index 709f42cd12..887d9ff1cd 100644
--- a/set.mm
+++ b/set.mm
@@ -30175,7 +30175,7 @@ generally appear in a single form (either definitional, but more often
   $}
 
   ${
-    $d z A $.  $d z B $.  $d x y C $.  $d x y z $.
+    $d z A $.  $d z B $.  $d x C $.  $d y C $.  $d x z $.  $d y z $.
     $( Rotate three restricted universal quantifiers.  (Contributed by AV,
        3-Dec-2021.) $)
     ralrot3 $p |- ( A. x e. A A. y e. B A. z e. C ph
@@ -30185,7 +30185,8 @@ generally appear in a single form (either definitional, but more often
   $}
 
   ${
-    $d w z A $.  $d w z B $.  $d w x y C $.  $d x y z D $.
+    $d w z A $.  $d w z B $.  $d w x C $.  $d w y C $.  $d x z D $.
+    $d y z D $.
     $( Rotate four restricted existential quantifiers twice.  (Contributed by
        NM, 8-Apr-2015.) $)
     rexrot4 $p |- ( E. x e. A E. y e. B E. z e. C E. w e. D ph
@@ -30221,7 +30222,7 @@ generally appear in a single form (either definitional, but more often
     NBDCMOAIJK $.
 
   ${
-    $d y A $.  $d x B $.  $d x y $.
+    $d y A $.  $d x y $.
     reeanlem.1 $e |- ( E. x E. y ( ( x e. A /\ ph ) /\ ( y e. B /\ ps ) )
                     <-> ( E. x ( x e. A /\ ph ) /\ E. y ( y e. B /\ ps ) ) ) $.
     $( Lemma factoring out common proof steps of ~ reeanv and ~ reean .
@@ -31200,8 +31201,8 @@ generally appear in a single form (either definitional, but more often
   $}
 
   ${
-    $d w ph $.  $d z ps $.  $d x ch $.  $d v ch $.  $d y u th $.  $d x A $.
-    $d w A $.  $d x y B $.  $d w y B $.  $d v B $.  $d x y z C $.
+    $d w ph $.  $d z ps $.  $d x ch $.  $d v ch $.  $d y th $.  $d u th $.
+    $d x A $.  $d w A $.  $d x y B $.  $d w y B $.  $d v B $.  $d x y z C $.
     $d w y z C $.  $d v z C $.  $d z y C $.  $d z C $.  $d u C $.
     cbvral3v.1 $e |- ( x = w -> ( ph <-> ch ) ) $.
     cbvral3v.2 $e |- ( y = v -> ( ch <-> th ) ) $.
@@ -31493,7 +31494,7 @@ generally appear in a single form (either definitional, but more often
   $}
 
   ${
-    $d A x y $.  $d ph x $.  $d ch y $.
+    $d x y $.  $d A y $.  $d ch y $.
     rabrabi.1 $e |- ( x = y -> ( ch <-> ph ) ) $.
     $( Abstract builder restricted to another restricted abstract builder with
        implicit substitution.  (Contributed by AV, 2-Aug-2022.)  Avoid
@@ -32401,7 +32402,7 @@ general is seen either by substitution (when the variable ` V ` has no
   $}
 
   ${
-    $d x y A $.  $d x y B $.  $d x y ps $.
+    $d x y $. $d x A $.  $d x y B $.  $d x y ps $.
     vtocl2.1 $e |- A e. _V $.
     vtocl2.2 $e |- B e. _V $.
     vtocl2.3 $e |- ( ( x = A /\ y = B ) -> ( ph <-> ps ) ) $.
@@ -32414,7 +32415,7 @@ general is seen either by substitution (when the variable ` V ` has no
   $}
 
   ${
-    $d x y z A $.  $d x y z B $.  $d x y z C $.  $d x y z ps $.
+    $d x y $.  $d x A $.  $d x y B $.  $d x y z C $.  $d x y z ps $.
     vtocl3.1 $e |- A e. _V $.
     vtocl3.2 $e |- B e. _V $.
     vtocl3.3 $e |- C e. _V $.
@@ -32427,7 +32428,7 @@ general is seen either by substitution (when the variable ` V ` has no
     vtocl3 $p |- ps $=
       ( cv wceq a1i wi wa wb 3expa pm5.74da vtocl2 2thd vtocl ) ABEHKENHOZABAUE
       MPZUEAQUEBQCDFGIJCNFOZDNGOZRUEABUGUHUEABSLTUAUFUBUCMUD $.
-    $( $j usage 'vtocl3' avoids 'ax-10' 'ax-11'; $)
+    $( $j usage 'vtocl3' avoids 'ax-10' 'ax-11' 'ax-12'; $)
   $}
 
   ${
@@ -32689,6 +32690,23 @@ general is seen either by substitution (when the variable ` V ` has no
       ( nfcv nfv vtocl3gaf ) ABCDEFGHIJKLMEHRFHRGHRFIRGIRGJRBESCFSDGSNOPQT $.
   $}
 
+  ${
+    $d A x $.  $d A y $.  $d B y $.  $d ps x $.  $d ch y $.  $d C z $.
+    $d C w $.  $d D w $.  $d A z $.  $d Q z $.  $d B z $.  $d R z $.
+    $d rh z $.  $d A w $.  $d Q w $.  $d B w $.  $d R w $.  $d th w $.
+    vtocl4g.1 $e |- ( x = A -> ( ph <-> ps ) ) $.
+    vtocl4g.2 $e |- ( y = B -> ( ps <-> ch ) ) $.
+    vtocl4g.3 $e |- ( z = C -> ( ch <-> rh ) ) $.
+    vtocl4g.4 $e |- ( w = D -> ( rh <-> th ) ) $.
+    vtocl4g.5 $e |- ph $.
+    $( Implicit substitution of 4 classes for 4 setvar variables.
+       (Contributed by AV, 22-Jan-2019.) $)
+    vtocl4g $p |- ( ( ( A e. Q /\ B e. R )
+                     /\ ( C e. S /\ D e. T ) ) -> th ) $=
+    ( wcel wa wi cv wceq imbi2d vtocl2g impcom ) LPUCMQUCUDJNUCKOUCUDZDUKCU
+    EUKEUEUKDUEHILMPQHUFLUGCEUKTUHIUFMUGEDUKUAUHABCFGJKNORSUBUIUIUJ $.
+  $}
+
   ${
     $d w x y z A $.  $d w y z B $.  $d w z C $.  $d w D $.  $d w x y z R $.
     $d w x y z S $.  $d w x y z T $.  $d w x y z Q $.  $d x ps $.  $d z rh $.
@@ -32697,16 +32715,6 @@ general is seen either by substitution (when the variable ` V ` has no
     vtocl4ga.2 $e |- ( y = B -> ( ps <-> ch ) ) $.
     vtocl4ga.3 $e |- ( z = C -> ( ch <-> rh ) ) $.
     vtocl4ga.4 $e |- ( w = D -> ( rh <-> th ) ) $.
-    ${
-      vtocl4g.5 $e |- ph $.
-      $( Implicit substitution of 4 classes for 4 setvar variables.
-         (Contributed by AV, 22-Jan-2019.) $)
-      vtocl4g $p |- ( ( ( A e. Q /\ B e. R )
-                       /\ ( C e. S /\ D e. T ) ) -> th ) $=
-        ( wcel wa wi cv wceq imbi2d vtocl2g impcom ) LPUCMQUCUDJNUCKOUCUDZDUKCU
-        EUKEUEUKDUEHILMPQHUFLUGCEUKTUHIUFMUGEDUKUAUHABCFGJKNORSUBUIUIUJ $.
-    $}
-
     vtocl4ga.5 $e |- ( ( ( x e. Q /\ y e. R )
                          /\ ( z e. S /\ w e. T ) ) -> ph ) $.
     $( Implicit substitution of 4 classes for 4 setvar variables.  (Contributed
@@ -34435,7 +34443,7 @@ general is seen either by substitution (when the variable ` V ` has no
     ( wreu wrmo wi wral reurmo rmoim syl5 ) BCDEBCDFABGCDHACDFBCDIABCDJK $.
 
   ${
-    $d x y A $.  $d x B $.
+    $d x y $.  $d y A $.  $d x B $.
     $( A condition allowing swap of uniqueness and existential quantifiers.
        (Contributed by Thierry Arnoux, 7-Apr-2017.)  (Revised by NM,
        16-Jun-2017.) $)
@@ -34451,7 +34459,7 @@ general is seen either by substitution (when the variable ` V ` has no
   $}
 
   ${
-    $d x y A $.  $d x B $.
+    $d x y $.  $d y A $.  $d x B $.
     $( A condition allowing swap of uniqueness and existential quantifiers.
        (Contributed by Thierry Arnoux, 7-Apr-2017.) $)
     2reuswap2 $p |- ( A. x e. A E* y ( y e. B /\ ph ) ->
@@ -34568,7 +34576,10 @@ general is seen either by substitution (when the variable ` V ` has no
       ( wrex wrmo nfcv nfre1 nfrmow wi wral cv wcel rmoim rspe ex syl11 ralrimi
       ralrimivw ) ACEFZBDGZABDGZCEUACBDCDHACEIJAUAKZBDLUBUCCMENZAUABDOUEUDBDUEA
       UAACEPQTRS $.
+  $}
 
+  ${
+    $d y A $.  $d x y $.
     $( Lemma for ~ 2reu5 .  Note that ` E! x e. A E! y e. B ph ` does not mean
        "there is exactly one ` x ` in ` A ` and exactly one ` y ` in ` B ` such
        that ` ph ` holds"; see comment for ~ 2eu5 .  (Contributed by Alexander
@@ -34628,6 +34639,13 @@ that existential restriction in the last conjunct (the "at most one"
       BCDEFGUNVQVOVBVQVKVPJZDLVOVPDFTWFVNDWFVLEGHVNVKVHEGUOVLEGTUPUQURUSUT $.
   $}
 
+  $( Double restricted quantification with restricted existential uniqueness
+     and restricted "at most one", analogous to ~ 2eumo .  (Contributed by
+     Alexander van der Vekens, 24-Jun-2017.) $)
+  2reurmo $p |- ( E! x e. A E* y e. B ph -> E* x e. A E! y e. B ph ) $=
+    ( wreu wrmo wi reuimrmo cv wcel reurmo a1i mprg ) ACEFZACEGZHZPBDFOBDGHBD
+    OPBDIQBJDKACELMN $.
+
   ${
     $d y A $.  $d x y $.  $d x B $.
     $( Double restricted quantification with existential uniqueness, analogous
@@ -34639,13 +34657,6 @@ that existential restriction in the last conjunct (the "at most one"
       LCOEPZUOUMQZULUPIABDHZUQUPULURUPAUJQZBDRULURQUPUSBDUPAUJACEUATUBAUJBDUCUD
       SABDUEUFTUGUHSUI $.
 
-    $( Double restricted quantification with restricted existential uniqueness
-       and restricted "at most one", analogous to ~ 2eumo .  (Contributed by
-       Alexander van der Vekens, 24-Jun-2017.) $)
-    2reurmo $p |- ( E! x e. A E* y e. B ph -> E* x e. A E! y e. B ph ) $=
-      ( wreu wrmo wi reuimrmo cv wcel reurmo a1i mprg ) ACEFZACEGZHZPBDFOBDGHBD
-      OPBDIQBJDKACELMN $.
-
     $( A condition allowing to swap restricted "at most one" and restricted
        existential quantifiers, analogous to ~ 2moswap .  (Contributed by
        Alexander van der Vekens, 25-Jun-2017.) $)
@@ -34820,7 +34831,7 @@ something like (wi (wceq (cv vx) (cv vy)) wph) ) into just (wcdeq vx vy
   $}
 
   ${
-    $d x ps $.  $d y ph $.
+    $d x ps $.
     nfcdeq.1 $e |- F/ x ph $.
     nfcdeq.2 $e |- CondEq ( x = y -> ( ph <-> ps ) ) $.
     $( If we have a conditional equality proof, where ` ph ` is ` ph ( x ) `
@@ -34835,7 +34846,7 @@ something like (wi (wceq (cv vx) (cv vy)) wph) ) into just (wcdeq vx vy
   $}
 
   ${
-    $d x z B $.  $d y z A $.
+    $d x z B $.  $d y z $. $d z A $.
     nfccdeq.1 $e |- F/_ x A $.
     nfccdeq.2 $e |- CondEq ( x = y -> A = B ) $.
     $( Variation of ~ nfcdeq for classes.  Usage of this theorem is discouraged
@@ -36047,7 +36058,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
   $}
 
   ${
-    $d x y A $.
+    $d x y $.  $d y A $.
     rmo2.1 $e |- F/ y ph $.
     $( Alternate definition of restricted "at most one."  Note that
        ` E* x e. A ph ` is not equivalent to
@@ -36065,6 +36076,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
       ( weq wi wral wrex wex wrmo rexex rmo2 sylibr ) ABCFGBDHZCDIOCJABDKOCDLAB
       CDEMN $.
 
+    $d x A $.
     $( Restricted "at most one" using explicit substitution.  (Contributed by
        NM, 4-Nov-2012.)  (Revised by NM, 16-Jun-2017.)  Avoid ~ ax-13 .
        (Revised by Wolf Lammen, 30-Apr-2023.) $)
@@ -36122,7 +36134,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
   $}
 
   ${
-    $d x y A $.  $d y ph $.  $d y ps $.
+    $d x y $.  $d y A $.  $d y ph $.  $d y ps $.
     rmoanim.1 $e |- F/ x ph $.
     $( Introduction of a conjunct into restricted "at most one" quantifier,
        analogous to ~ moanim .  (Contributed by Alexander van der Vekens,
@@ -36158,7 +36170,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
   $}
 
   ${
-    $d x y A $.  $d x B $.
+    $d x y $.  $d y A $.  $d x B $.
     $( Double restricted existential uniqueness.  This theorem shows a
        condition under which a "naive" definition matches the correct one,
        analogous to ~ 2eu1 .  (Contributed by Alexander van der Vekens,
@@ -36553,7 +36565,7 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
   $}
 
   ${
-    $d x A $.  $d x V $.
+    $d x A $.
     csbiegf.1 $e |- ( A e. V -> F/_ x C ) $.
     csbiegf.2 $e |- ( x = A -> B = C ) $.
     $( Conversion of implicit substitution to explicit substitution into a
@@ -39659,6 +39671,15 @@ technically classes despite morally (and provably) being sets, like ` 1 `
 -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
 $)
 
+  $( Transfer uniqueness to a smaller or larger class.  (Contributed by NM,
+     21-Oct-2005.) $)
+  reuun2 $p |- ( -. E. x e. B ph ->
+           ( E! x e. ( A u. B ) ph <-> E! x e. A ph ) ) $=
+    ( wrex wn cv wcel wa wo weu cun wreu wex df-rex euor2 sylnbi df-reu bitri
+    wb elun anbi1i andir orcom eubii 3bitr4g ) ABDEZFBGZDHZAIZUHCHZAIZJZBKZUL
+    BKZABCDLZMZABCMUGUJBNUNUOTABDOUJULBPQUQUHUPHZAIZBKUNABUPRUSUMBUSUKUIJZAIZ
+    UMURUTAUHCDUAUBVAULUJJUMUKUIAUCULUJUDSSUESABCRUF $.
+
   ${
     $d x A $.  $d x B $.
     $( Transfer uniqueness to a smaller subclass.  (Contributed by NM,
@@ -39686,15 +39707,6 @@ technically classes despite morally (and provably) being sets, like ` 1 `
       ( cun wss wo wi wral wrex wreu wa ssun1 orc rgenw reuss2 mpanl12 ) DDEFZG
       AABHZIZCDJACDKTCSLMACDLDENUACDABOPATCDSQR $.
 
-    $( Transfer uniqueness to a smaller or larger class.  (Contributed by NM,
-       21-Oct-2005.) $)
-    reuun2 $p |- ( -. E. x e. B ph ->
-             ( E! x e. ( A u. B ) ph <-> E! x e. A ph ) ) $=
-      ( wrex wn cv wcel wa wo weu cun wreu wex df-rex euor2 sylnbi df-reu bitri
-      wb elun anbi1i andir orcom eubii 3bitr4g ) ABDEZFBGZDHZAIZUHCHZAIZJZBKZUL
-      BKZABCDLZMZABCMUGUJBNUNUOTABDOUJULBPQUQUHUPHZAIZBKUNABUPRUSUMBUSUKUIJZAIZ
-      UMURUTAUHCDUAUBVAULUJJUMUKUIAUCULUJUDSSUESABCRUF $.
-
     $( Restricted uniqueness "picks" a member of a subclass.  (Contributed by
        NM, 21-Aug-1999.) $)
     reupick $p |- ( ( ( A C_ B /\ ( E. x e. A ph /\ E! x e. B ph ) ) /\ ph ) ->
@@ -40297,14 +40309,14 @@ among classes ( ~ eq0 , as opposed to the weaker uniqueness among sets,
     rabxm $p |- A = ( { x e. A | ph } u. { x e. A | -. ph } ) $=
       ( wn wo crab cun wceq rabid2 cv wcel exmidd mprgbir unrab eqtr4i ) CAADZE
       ZBCFZABCFPBCFGCRHQBCQBCIBJCKALMAPBCNO $.
-
-    $( Law of noncontradiction, in terms of restricted class abstractions.
-       (Contributed by Jeff Madsen, 20-Jun-2011.) $)
-    rabnc $p |- ( { x e. A | ph } i^i { x e. A | -. ph } ) = (/) $=
-      ( crab wn cin wa c0 inrab wceq wral pm3.24 rgenw rabeq0 mpbir eqtri ) ABC
-      DAEZBCDFAQGZBCDZHAQBCISHJREZBCKTBCALMRBCNOP $.
   $}
 
+  $( Law of noncontradiction, in terms of restricted class abstractions.
+     (Contributed by Jeff Madsen, 20-Jun-2011.) $)
+  rabnc $p |- ( { x e. A | ph } i^i { x e. A | -. ph } ) = (/) $=
+    ( crab wn cin wa c0 inrab wceq wral pm3.24 rgenw rabeq0 mpbir eqtri ) ABC
+    DAEZBCDFAQGZBCDZHAQBCISHJREZBCKTBCALMRBCNOP $.
+
   ${
     $d A s $.
     elneldisj.e $e |- E = { s e. A | B e. C } $.
@@ -41404,17 +41416,17 @@ disjoint classes (see ~ disjdif ).  Part of proof of Corollary 6K of
       ( wrex c0 wn wral wceq dfrex2 rzal con3i sylbi neqned ) ABCDZCENAFZBCGZFC
       EHZFABCIQPOBCJKLM $.
     $( $j usage 'rexn0' avoids 'df-clel' 'ax-8'; $)
-
-    $( Idempotent law for restricted quantifier.  (Contributed by NM,
-       28-Mar-1997.)  Reduce axiom usage.  (Revised by Gino Giotto,
-       2-Sep-2024.) $)
-    ralidm $p |- ( A. x e. A A. x e. A ph <-> A. x e. A ph ) $=
-      ( wral cv wcel wi wal df-ral ax-1 axc4i pm2.21 sp ja impbii bicomi imbi2i
-      alimi albii 3bitrri bitri ) ABCDZBCDBECFZUBGZBHZUBUBBCIUBUCAGZBHZUCUGGZBH
-      ZUEABCIZUGUIUFUHBUGUCJKUHUFBUCUGUFUCALUFBMNROUHUDBUGUBUCUBUGUJPQSTUA $.
-    $( $j usage 'ralidm' avoids 'df-clel' 'df-cleq' 'ax-8' 'ax-9' 'ax-ext'; $)
   $}
 
+  $( Idempotent law for restricted quantifier.  (Contributed by NM,
+     28-Mar-1997.)  Reduce axiom usage.  (Revised by Gino Giotto,
+     2-Sep-2024.) $)
+  ralidm $p |- ( A. x e. A A. x e. A ph <-> A. x e. A ph ) $=
+    ( wral cv wcel wi wal df-ral ax-1 axc4i pm2.21 sp ja impbii bicomi imbi2i
+    alimi albii 3bitrri bitri ) ABCDZBCDBECFZUBGZBHZUBUBBCIUBUCAGZBHZUCUGGZBH
+    ZUEABCIZUGUIUFUHBUGUCJKUHUFBUCUGUFUCALUFBMNROUHUDBUGUBUCUBUGUJPQSTUA $.
+  $( $j usage 'ralidm' avoids 'df-clel' 'df-cleq' 'ax-8' 'ax-9' 'ax-ext'; $)
+
   $( Vacuous universal quantification is always true.  (Contributed by NM,
      20-Oct-2005.)  Avoid ~ df-clel , ~ ax-8 .  (Revised by Gino Giotto,
      2-Sep-2024.) $)
@@ -41538,7 +41550,7 @@ disjoint classes (see ~ disjdif ).  Part of proof of Corollary 6K of
   $}
 
   ${
-    $d x y A $.  $d x y B $.
+    $d x y $.  $d x A $.  $d x y B $.
     raaan2.1 $e |- F/ y ph $.
     raaan2.2 $e |- F/ x ps $.
     $( Rearrange restricted quantifiers with two different restricting classes,
@@ -44084,17 +44096,14 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ).
     wa imbi2i 3bitri ralbii2 ) AEZABFZDGZHZBCDIJZCUDUGKZUCHUDCKZUDDLZSZUCHUIUJU
     CHZHUIUFHUHUKUCUDCDMNUIUJUCOULUFUIULUEEZUCHUFUJUMUCUDDPNAUEQRTUAUB $.
 
-  ${
-    $d x Y $.
-    $( Restricted universal quantification on a class difference with a
-       singleton in terms of an implication.  (Contributed by Alexander van der
-       Vekens, 26-Jan-2018.) $)
-    raldifsnb $p |- ( A. x e. A ( x =/= Y -> ph )
-                      <-> A. x e. ( A \ { Y } ) ph ) $=
-      ( cv wne wi wral csn wnel cdif wcel wceq wn velsn nnel nne con4bii imbi1i
-      3bitr4ri ralbii raldifb bitri ) BEZDFZAGZBCHUDDIZJZAGZBCHABCUGKHUFUIBCUEU
-      HAUEUHUDUGLUDDMUHNUENBDOUDUGPUDDQTRSUAABCUGUBUC $.
-  $}
+  $( Restricted universal quantification on a class difference with a
+     singleton in terms of an implication.  (Contributed by Alexander van der
+     Vekens, 26-Jan-2018.) $)
+  raldifsnb $p |- ( A. x e. A ( x =/= Y -> ph )
+                    <-> A. x e. ( A \ { Y } ) ph ) $=
+    ( cv wne wi wral csn wnel cdif wcel wceq wn velsn nnel nne con4bii imbi1i
+    3bitr4ri ralbii raldifb bitri ) BEZDFZAGZBCHUDDIZJZAGZBCHABCUGKHUFUIBCUEU
+    HAUEUHUDUGLUDDMUHNUENBDOUDUGPUDDQTRSUAABCUGUBUC $.
 
   $( A set is an element of the universal class excluding a singleton iff it is
      not the singleton element.  (Contributed by AV, 7-Apr-2019.) $)
@@ -44366,7 +44375,7 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ).
   $}
 
   ${
-    $d A w x y z $.
+    $d A w x y $.  $d A w x z $.
     $( A sufficient condition for a (nonempty) set to be a singleton.
        (Contributed by AV, 20-Sep-2020.) $)
     issn $p |- ( E. x e. A A. y e. A x = y -> E. z A = { z } ) $=
@@ -44374,7 +44383,10 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ).
       c0 bitr4d sneq eqeq2d spcegv sylbid rexlimiv ) ABEZBDFZDCGZHZIZCJZADAGZDK
       ZUHDUMHZIZULUNUHBAEZBDFZUPUNUGUQBDUGUQLUNABMNOUNDTPUPURLDUMQBDUMRSUAUKUPC
       UMDCAEUJUODUIUMUBUCUDUEUF $.
+  $}
 
+  ${
+    $d A w y x $.  $d A w y z $.
     $( A nonempty set is either a singleton or contains at least two different
        elements.  (Contributed by AV, 20-Sep-2020.) $)
     n0snor2el $p |- ( A =/= (/)
@@ -46222,7 +46234,7 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and
   $}
 
   ${
-    $d x ph $.  $d x A $.
+    $d x ph $.
     iuneq2d.2 $e |- ( ph -> B = C ) $.
     $( Equality deduction for indexed union.  (Contributed by Drahflow,
        22-Oct-2015.) $)

From 829e375e40922e2709ad4652d75be0da4ed6a52e Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Mon, 14 Oct 2024 14:16:08 +0200
Subject: [PATCH 2/4] rewrap

---
 set.mm | 30 +++++++++++++++---------------
 1 file changed, 15 insertions(+), 15 deletions(-)

diff --git a/set.mm b/set.mm
index 887d9ff1cd..e74e86b718 100644
--- a/set.mm
+++ b/set.mm
@@ -32703,8 +32703,8 @@ general is seen either by substitution (when the variable ` V ` has no
        (Contributed by AV, 22-Jan-2019.) $)
     vtocl4g $p |- ( ( ( A e. Q /\ B e. R )
                      /\ ( C e. S /\ D e. T ) ) -> th ) $=
-    ( wcel wa wi cv wceq imbi2d vtocl2g impcom ) LPUCMQUCUDJNUCKOUCUDZDUKCU
-    EUKEUEUKDUEHILMPQHUFLUGCEUKTUHIUFMUGEDUKUAUHABCFGJKNORSUBUIUIUJ $.
+      ( wcel wa wi cv wceq imbi2d vtocl2g impcom ) LPUCMQUCUDJNUCKOUCUDZDUKCUEU
+      KEUEUKDUEHILMPQHUFLUGCEUKTUHIUFMUGEDUKUAUHABCFGJKNORSUBUIUIUJ $.
   $}
 
   ${
@@ -34643,8 +34643,8 @@ that existential restriction in the last conjunct (the "at most one"
      and restricted "at most one", analogous to ~ 2eumo .  (Contributed by
      Alexander van der Vekens, 24-Jun-2017.) $)
   2reurmo $p |- ( E! x e. A E* y e. B ph -> E* x e. A E! y e. B ph ) $=
-    ( wreu wrmo wi reuimrmo cv wcel reurmo a1i mprg ) ACEFZACEGZHZPBDFOBDGHBD
-    OPBDIQBJDKACELMN $.
+    ( wreu wrmo wi reuimrmo cv wcel reurmo a1i mprg ) ACEFZACEGZHZPBDFOBDGHBDOP
+    BDIQBJDKACELMN $.
 
   ${
     $d y A $.  $d x y $.  $d x B $.
@@ -39676,9 +39676,9 @@ technically classes despite morally (and provably) being sets, like ` 1 `
   reuun2 $p |- ( -. E. x e. B ph ->
            ( E! x e. ( A u. B ) ph <-> E! x e. A ph ) ) $=
     ( wrex wn cv wcel wa wo weu cun wreu wex df-rex euor2 sylnbi df-reu bitri
-    wb elun anbi1i andir orcom eubii 3bitr4g ) ABDEZFBGZDHZAIZUHCHZAIZJZBKZUL
-    BKZABCDLZMZABCMUGUJBNUNUOTABDOUJULBPQUQUHUPHZAIZBKUNABUPRUSUMBUSUKUIJZAIZ
-    UMURUTAUHCDUAUBVAULUJJUMUKUIAUCULUJUDSSUESABCRUF $.
+    wb elun anbi1i andir orcom eubii 3bitr4g ) ABDEZFBGZDHZAIZUHCHZAIZJZBKZULBK
+    ZABCDLZMZABCMUGUJBNUNUOTABDOUJULBPQUQUHUPHZAIZBKUNABUPRUSUMBUSUKUIJZAIZUMUR
+    UTAUHCDUAUBVAULUJJUMUKUIAUCULUJUDSSUESABCRUF $.
 
   ${
     $d x A $.  $d x B $.
@@ -40314,8 +40314,8 @@ among classes ( ~ eq0 , as opposed to the weaker uniqueness among sets,
   $( Law of noncontradiction, in terms of restricted class abstractions.
      (Contributed by Jeff Madsen, 20-Jun-2011.) $)
   rabnc $p |- ( { x e. A | ph } i^i { x e. A | -. ph } ) = (/) $=
-    ( crab wn cin wa c0 inrab wceq wral pm3.24 rgenw rabeq0 mpbir eqtri ) ABC
-    DAEZBCDFAQGZBCDZHAQBCISHJREZBCKTBCALMRBCNOP $.
+    ( crab wn cin wa c0 inrab wceq wral pm3.24 rgenw rabeq0 mpbir eqtri ) ABCDA
+    EZBCDFAQGZBCDZHAQBCISHJREZBCKTBCALMRBCNOP $.
 
   ${
     $d A s $.
@@ -41422,9 +41422,9 @@ disjoint classes (see ~ disjdif ).  Part of proof of Corollary 6K of
      28-Mar-1997.)  Reduce axiom usage.  (Revised by Gino Giotto,
      2-Sep-2024.) $)
   ralidm $p |- ( A. x e. A A. x e. A ph <-> A. x e. A ph ) $=
-    ( wral cv wcel wi wal df-ral ax-1 axc4i pm2.21 sp ja impbii bicomi imbi2i
-    alimi albii 3bitrri bitri ) ABCDZBCDBECFZUBGZBHZUBUBBCIUBUCAGZBHZUCUGGZBH
-    ZUEABCIZUGUIUFUHBUGUCJKUHUFBUCUGUFUCALUFBMNROUHUDBUGUBUCUBUGUJPQSTUA $.
+    ( wral cv wcel wi df-ral ax-1 axc4i pm2.21 sp ja alimi impbii bicomi imbi2i
+    wal albii 3bitrri bitri ) ABCDZBCDBECFZUBGZBRZUBUBBCHUBUCAGZBRZUCUGGZBRZUEA
+    BCHZUGUIUFUHBUGUCIJUHUFBUCUGUFUCAKUFBLMNOUHUDBUGUBUCUBUGUJPQSTUA $.
   $( $j usage 'ralidm' avoids 'df-clel' 'df-cleq' 'ax-8' 'ax-9' 'ax-ext'; $)
 
   $( Vacuous universal quantification is always true.  (Contributed by NM,
@@ -44101,9 +44101,9 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ).
      Vekens, 26-Jan-2018.) $)
   raldifsnb $p |- ( A. x e. A ( x =/= Y -> ph )
                     <-> A. x e. ( A \ { Y } ) ph ) $=
-    ( cv wne wi wral csn wnel cdif wcel wceq wn velsn nnel nne con4bii imbi1i
-    3bitr4ri ralbii raldifb bitri ) BEZDFZAGZBCHUDDIZJZAGZBCHABCUGKHUFUIBCUEU
-    HAUEUHUDUGLUDDMUHNUENBDOUDUGPUDDQTRSUAABCUGUBUC $.
+    ( cv wne wi wral csn wnel cdif wcel wceq wn velsn nnel nne 3bitr4ri con4bii
+    imbi1i ralbii raldifb bitri ) BEZDFZAGZBCHUDDIZJZAGZBCHABCUGKHUFUIBCUEUHAUE
+    UHUDUGLUDDMUHNUENBDOUDUGPUDDQRSTUAABCUGUBUC $.
 
   $( A set is an element of the universal class excluding a singleton iff it is
      not the singleton element.  (Contributed by AV, 7-Apr-2019.) $)

From 37698507ab5048b461cd4f4c70e2a107a0047d9d Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Mon, 14 Oct 2024 14:19:38 +0200
Subject: [PATCH 3/4] rewrap

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

diff --git a/set.mm b/set.mm
index e74e86b718..182e7238e9 100644
--- a/set.mm
+++ b/set.mm
@@ -32402,7 +32402,7 @@ general is seen either by substitution (when the variable ` V ` has no
   $}
 
   ${
-    $d x y $. $d x A $.  $d x y B $.  $d x y ps $.
+    $d x y $.  $d x A $.  $d x y B $.  $d x y ps $.
     vtocl2.1 $e |- A e. _V $.
     vtocl2.2 $e |- B e. _V $.
     vtocl2.3 $e |- ( ( x = A /\ y = B ) -> ( ph <-> ps ) ) $.
@@ -32699,8 +32699,8 @@ general is seen either by substitution (when the variable ` V ` has no
     vtocl4g.3 $e |- ( z = C -> ( ch <-> rh ) ) $.
     vtocl4g.4 $e |- ( w = D -> ( rh <-> th ) ) $.
     vtocl4g.5 $e |- ph $.
-    $( Implicit substitution of 4 classes for 4 setvar variables.
-       (Contributed by AV, 22-Jan-2019.) $)
+    $( Implicit substitution of 4 classes for 4 setvar variables.  (Contributed
+       by AV, 22-Jan-2019.) $)
     vtocl4g $p |- ( ( ( A e. Q /\ B e. R )
                      /\ ( C e. S /\ D e. T ) ) -> th ) $=
       ( wcel wa wi cv wceq imbi2d vtocl2g impcom ) LPUCMQUCUDJNUCKOUCUDZDUKCUEU
@@ -34846,7 +34846,7 @@ something like (wi (wceq (cv vx) (cv vy)) wph) ) into just (wcdeq vx vy
   $}
 
   ${
-    $d x z B $.  $d y z $. $d z A $.
+    $d x z B $.  $d y z $.  $d z A $.
     nfccdeq.1 $e |- F/_ x A $.
     nfccdeq.2 $e |- CondEq ( x = y -> A = B ) $.
     $( Variation of ~ nfcdeq for classes.  Usage of this theorem is discouraged
@@ -44096,9 +44096,9 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ).
     wa imbi2i 3bitri ralbii2 ) AEZABFZDGZHZBCDIJZCUDUGKZUCHUDCKZUDDLZSZUCHUIUJU
     CHZHUIUFHUHUKUCUDCDMNUIUJUCOULUFUIULUEEZUCHUFUJUMUCUDDPNAUEQRTUAUB $.
 
-  $( Restricted universal quantification on a class difference with a
-     singleton in terms of an implication.  (Contributed by Alexander van der
-     Vekens, 26-Jan-2018.) $)
+  $( Restricted universal quantification on a class difference with a singleton
+     in terms of an implication.  (Contributed by Alexander van der Vekens,
+     26-Jan-2018.) $)
   raldifsnb $p |- ( A. x e. A ( x =/= Y -> ph )
                     <-> A. x e. ( A \ { Y } ) ph ) $=
     ( cv wne wi wral csn wnel cdif wcel wceq wn velsn nnel nne 3bitr4ri con4bii

From cd68be7c527b23323013ac148af29267cac97d24 Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Mon, 14 Oct 2024 14:42:08 +0200
Subject: [PATCH 4/4] remove additional DV condition

---
 set.mm | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/set.mm b/set.mm
index 182e7238e9..da46d0abcb 100644
--- a/set.mm
+++ b/set.mm
@@ -44386,7 +44386,7 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ).
   $}
 
   ${
-    $d A w y x $.  $d A w y z $.
+    $d A w y x $.  $d A w y $.  $d A w z $.
     $( A nonempty set is either a singleton or contains at least two different
        elements.  (Contributed by AV, 20-Sep-2020.) $)
     n0snor2el $p |- ( A =/= (/)