diff --git a/set.mm b/set.mm
index fb3eae8622..6a03a31ca8 100644
--- a/set.mm
+++ b/set.mm
@@ -450801,12 +450801,12 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the
 htmldef "ErALTV" as ' ErALTV ';
   althtmldef "ErALTV" as ' ErALTV ';
   latexdef "ErALTV" as "\mathrm{ErALTV}";
-htmldef "MembErs" as ' MembErs ';
-  althtmldef "MembErs" as ' MembErs ';
-  latexdef "MembErs" as "\mathrm{MembErs}";
-htmldef "MembEr" as ' MembEr ';
-  althtmldef "MembEr" as ' MembEr ';
-  latexdef "MembEr" as "\mathrm{MembEr}";
+htmldef "CoMembErs" as ' CoMembErs ';
+  althtmldef "CoMembErs" as ' CoMembErs ';
+  latexdef "CoMembErs" as "\mathrm{CoMembErs}";
+htmldef "CoMembEr" as ' CoMembEr ';
+  althtmldef "CoMembEr" as ' CoMembEr ';
+  latexdef "CoMembEr" as "\mathrm{CoMembEr}";
 htmldef "Funss" as ' Funss ';
   althtmldef "Funss" as ' Funss ';
   latexdef "Funss" as "\mathrm{Funss}";
@@ -580791,8 +580791,8 @@ A collection of theorems for commuting equalities (or
                quotients $)
   $c ErALTV $. $( Equivalence relation on its domain quotient predicate $)
 
-  $c MembErs $. $( The class of membership equivalence relations $)
-  $c MembEr $. $( Membership equivalence relation predicate $)
+  $c CoMembErs $. $( The class of comembership equivalence relations $)
+  $c CoMembEr $. $( Comembership equivalence relation predicate $)
 
   $c Funss $. $( The class of all function sets (used only once) $)
   $c FunsALTV $. $( The class of functions, i.e., function relations $)
@@ -580907,14 +580907,14 @@ A collection of theorems for commuting equalities (or
      domain quotient ` A ` .) $)
   werALTV $a wff R ErALTV A $.
 
-  $( Extend the definition of a class to include the membership equivalence
+  $( Extend the definition of a class to include the comembership equivalence
      relations class. $)
-  cmembers $a class MembErs $.
-  $( Extend the definition of a wff to include the membership equivalence
-     relation predicate.  (Read: the membership equivalence relation on ` A ` ,
-     or, the restricted elementhood equivalence relation on its domain quotient
-     ` A ` .) $)
-  wmember $a wff MembEr A $.
+  ccomembers $a class CoMembErs $.
+  $( Extend the definition of a wff to include the comembership equivalence
+     relation predicate.  (Read: the comembership equivalence relation on
+     ` A ` , or, the restricted coelement equivalence relation on its domain
+     quotient ` A ` .) $)
+  wcomember $a wff CoMembEr A $.
 
   $( Extend the definition of a class to include the function set class. $)
   cfunss $a class Funss $.
@@ -585491,21 +585491,21 @@ reflexive relation (see ~ dfrefrel3 ) in equivalence relation.
      ~ brerser .  (Contributed by Peter Mazsa, 12-Aug-2021.) $)
   df-erALTV $a |- ( R ErALTV A <-> ( EqvRel R /\ R DomainQs A ) ) $.
 
-  $( Define the class of membership equivalence relations on their domain
+  $( Define the class of comembership equivalence relations on their domain
      quotients.  (Contributed by Peter Mazsa, 28-Nov-2022.)  (Revised by Peter
      Mazsa, 24-Jul-2023.) $)
-  df-members $a |- MembErs = { a | ,~ ( `' _E |` a ) Ers a } $.
+  df-comembers $a |- CoMembErs = { a | ,~ ( `' _E |` a ) Ers a } $.
 
-  $( Define the membership equivalence relation on the class ` A ` (or, the
-     restricted elementhood equivalence relation on its domain quotient
-     ` A ` .)  Alternate definitions are ~ dfmember2 and ~ dfmember3 .
+  $( Define the comembership equivalence relation on the class ` A ` (or, the
+     restricted coelement equivalence relation on its domain quotient ` A ` .)
+     Alternate definitions are ~ dfcomember2 and ~ dfcomember3 .
 
      Later on, in an application of set theory I make a distinction between the
      default elementhood concept and a special membership concept: membership
      equivalence relation will be an integral part of that membership concept.
      (Contributed by Peter Mazsa, 26-Jun-2021.)  (Revised by Peter Mazsa,
      28-Nov-2022.) $)
-  df-member $a |- ( MembEr A <-> ,~ ( `' _E |` A ) ErALTV A ) $.
+  df-comember $a |- ( CoMembEr A <-> ,~ ( `' _E |` A ) ErALTV A ) $.
 
   $( Binary equivalence relation with natural domain, see the comment of
      ~ df-ers .  (Contributed by Peter Mazsa, 23-Jul-2021.) $)
@@ -585544,22 +585544,25 @@ reflexive relation (see ~ dfrefrel3 ) in equivalence relation.
 
   $( Alternate definition of the membership equivalence relation.  (Contributed
      by Peter Mazsa, 28-Nov-2022.) $)
-  dfmember $p |- ( MembEr A <-> ~ A ErALTV A ) $=
-    ( wmember cep ccnv cres werALTV ccoels df-member df-coels erALTVeq1i bitr4i
-    ccoss ) ABACDAELZFAAGZFAHANMAIJK $.
-
-  $( Alternate definition of the membership equivalence relation.  (Contributed
-     by Peter Mazsa, 25-Sep-2021.) $)
-  dfmember2 $p |- ( MembEr A <-> ( EqvRel ~ A /\ ( dom ~ A /. ~ A ) = A ) ) $=
-    ( wmember ccoels werALTV weqvrel cdm cqs wceq wa dfmember dferALTV2 bitri )
-    ABAACZDMEMFMGAHIAJAMKL $.
+  dfcomember $p |- ( CoMembEr A <-> ~ A ErALTV A ) $=
+    ( wcomember ccnv cres werALTV ccoels df-comember df-coels erALTVeq1i bitr4i
+    cep ccoss ) ABAKCADLZEAAFZEAGANMAHIJ $.
 
-  $( Alternate definition of the membership equivalence relation.  (Contributed
-     by Peter Mazsa, 26-Sep-2021.)  (Revised by Peter Mazsa, 17-Jul-2023.) $)
-  dfmember3 $p |- ( MembEr A <-> ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) ) $=
-    ( wmember ccoels weqvrel cdm cqs wceq wa wcoeleqvrel dfmember2 dfcoeleqvrel
-    cuni bicomi dmqscoelseq anbi12i bitri ) ABACZDZQEQFAGZHAIZALQFAGZHAJRTSUATR
-    AKMANOP $.
+  $( Alternate definition of the comembership equivalence relation.
+     (Contributed by Peter Mazsa, 25-Sep-2021.) $)
+  dfcomember2 $p |- ( CoMembEr A <->
+                      ( EqvRel ~ A /\ ( dom ~ A /. ~ A ) = A ) ) $=
+    ( wcomember ccoels werALTV weqvrel cdm cqs wceq dfcomember dferALTV2 bitri
+    wa ) ABAACZDMEMFMGAHLAIAMJK $.
+
+  $( Alternate definition of the comembership equivalence relation.
+     (Contributed by Peter Mazsa, 26-Sep-2021.)  (Revised by Peter Mazsa,
+     17-Jul-2023.) $)
+  dfcomember3 $p |- ( CoMembEr A <->
+                      ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) ) $=
+    ( wcomember ccoels weqvrel cdm wceq wa wcoeleqvrel dfcomember2 dfcoeleqvrel
+    cqs cuni bicomi dmqscoelseq anbi12i bitri ) ABACZDZQEQKAFZGAHZALQKAFZGAIRTS
+    UATRAJMANOP $.
 
   $( Two ways to express membership equivalence relation on its domain
      quotient.  (Contributed by Peter Mazsa, 26-Sep-2021.)  (Revised by Peter