From 6774571e24e23afab839cc382243f259b38d2982 Mon Sep 17 00:00:00 2001
From: mazsa <peter@mazsa.com>
Date: Sun, 12 Jan 2025 14:11:26 +0100
Subject: [PATCH] undif5 to main

---
 set.mm | 19 ++++++-------------
 1 file changed, 6 insertions(+), 13 deletions(-)

diff --git a/set.mm b/set.mm
index 7ed29919c..bd3025843 100644
--- a/set.mm
+++ b/set.mm
@@ -41684,6 +41684,11 @@ disjoint classes (see ~ disjdif ).  Part of proof of Corollary 6K of
     ( wss cun wceq cdif ssequn1 undif2 eqeq1i bitr4i ) ABCABDZBEABAFDZBEABGLKBA
     BHIJ $.
 
+  $( An equality involving class union and class difference.  (Contributed by
+     Thierry Arnoux, 26-Jun-2024.) $)
+  undif5 $p |- ( ( A i^i B ) = (/) -> ( ( A u. B ) \ B ) = A ) $=
+    ( cin c0 wceq cun cdif difun2 disjdif2 eqtrid ) ABCDEABFBGABGAABHABIJ $.
+
   $( A subset of a difference does not intersect the subtrahend.  (Contributed
      by Jeff Hankins, 1-Sep-2013.)  (Proof shortened by Mario Carneiro,
      24-Aug-2015.) $)
@@ -473562,11 +473567,6 @@ Class abstractions (a.k.a. class builders)
     ( wceq wss wa cdif c0 eqss ssdif0 anbi12i sylbbr ) ABCABDZBADZEABFGCZBAFGCZ
     EABHLNMOABIBAIJK $.
 
-  $( An equality involving class union and class difference.  (Contributed by
-     Thierry Arnoux, 26-Jun-2024.) $)
-  undif5 $p |- ( ( A i^i B ) = (/) -> ( ( A u. B ) \ B ) = A ) $=
-    ( cin c0 wceq cun cdif difun2 disjdif2 eqtrid ) ABCDEABFBGABGAABHABIJ $.
-
   $( Two ways to express equality relative to a class ` A ` .  (Contributed by
      Thierry Arnoux, 23-Jun-2024.) $)
   indifbi $p |- ( ( A i^i B ) = ( A i^i C ) <-> ( A \ B ) = ( A \ C ) ) $=
@@ -581500,17 +581500,10 @@ A collection of theorems for commuting equalities (or
   suceqsneq $p |- ( A e. V -> ( suc A = suc B <-> { A } = { B } ) ) $=
     ( wcel csuc wceq csn suc11reg sneqbg bitr4id ) ACDAEBEFABFAGBGFABHABCIJ $.
 
-  $( An equality involving class union and class difference.  (Temporary: as
-     soon as this Mathbox only PR is accepted, I'll open a PR to place this to
-     the main.  PM) (Contributed by Thierry Arnoux, 26-Jun-2024.) $)
-  undif5TEMP $p |- ( ( A i^i B ) = (/) -> ( ( A u. B ) \ B ) = A ) $=
-    ( cin c0 wceq cun cdif difun2 disjdif2 eqtrid ) ABCDEABFBGABGAABHABIJ $.
-
   $( Absorption of union with a singleton by difference.  (Contributed by Peter
      Mazsa, 24-Jul-2024.) $)
   sucdifsn2 $p |- ( ( A u. { A } ) \ { A } ) = A $=
-    ( csn cin c0 wceq cun cdif disjcsn undif5TEMP ax-mp ) AABZCDEAKFKGAEAHAKIJ
-    $.
+    ( csn cin c0 wceq cun cdif disjcsn undif5 ax-mp ) AABZCDEAKFKGAEAHAKIJ $.
 
   $( The difference between the successor and the singleton of a class is the
      class.  (Contributed by Peter Mazsa, 20-Sep-2024.) $)