From 4f7570b89d50a63a8ea77b7dbde280b4126bc3ce Mon Sep 17 00:00:00 2001
From: mazsa <peter@mazsa.com>
Date: Thu, 2 Jan 2025 14:21:57 +0100
Subject: [PATCH] suceqsneq

---
 set.mm | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/set.mm b/set.mm
index 0cef0f8c25..8378ec79d6 100644
--- a/set.mm
+++ b/set.mm
@@ -580908,6 +580908,11 @@ A collection of theorems for commuting equalities (or
       ( wceq wb eqeq12 sylan2 ) ABCGDEGBDGCEGHFBCDEIJ $.
   $}
 
+  $( One-to-one relationship between the successor operation and the singleton.
+     (Contributed by Peter Mazsa, 31-Dec-2024.) $)
+  suceqsneq $p |- ( A e. V -> ( suc A = suc B <-> { A } = { B } ) ) $=
+    ( wcel csuc wceq csn suc11reg sneqbg bitr4id ) ACDAEBEFABFAGBGFABHABCIJ $.
+
   $( Two ways of expressing the restriction of an intersection.  (Contributed
      by Peter Mazsa, 5-Jun-2021.) $)
   inres2 $p |- ( ( R |` A ) i^i S ) = ( ( R i^i S ) |` A ) $=