suceqsneq

mazsa · Jan 2, 2025 · 6a583e2 · 6a583e2
1 parent a69a0a9
commit 6a583e2
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/set.mm b/set.mm
@@ -581045,6 +581045,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 ) $=