diff --git a/set.mm b/set.mm
index b8f10eae83..70d795e8eb 100644
--- a/set.mm
+++ b/set.mm
@@ -550481,11 +550481,23 @@ A collection of theorems for commuting equalities (or
     mpbir ) ABCEAFZBDEGZHIARJZBCDGZEZHIZUCTFZBUAKUDBUAALMTBUANQSUBHAR
     BCDOPQ $.
 
+  $( Substitution of equal classes into binary relation.  (Contributed by
+     Peter Mazsa, 14-Jun-2024.) $)
+  eqbrtr $p |- ( ( A = B /\ B R C ) -> A R C ) $=
+    ( wceq wbr breq1 biimpar ) ABEACDFBCDFABCDGH $.
+
   $( Substitution of equal classes into elementhood relation.  (Contributed by
      Peter Mazsa, 22-Jul-2017.) $)
   eqeltr $p |- ( ( A = B /\ B e. C ) -> A e. C ) $=
     ( wceq wcel eleq1 biimpar ) ABDACEBCEABCFG $.
 
+  $( Substitution of equal classes into binary relation.  (Contributed by
+     Peter Mazsa, 14-Jun-2024.) $)
+  eqbrb $p |- ( ( A = B /\ A R C ) <-> ( A = B /\ B R C ) ) $=
+    ( wceq wbr wa simpl eqbrtr jca eqcom anbi1i 3imtr3i impbii ) ABEZ
+    ACDFZGZOBCDFZGZBAEZPGZTRGQSUATRTPHBACDIJTOPBAKZLTORUBLMSOPORHABCD
+    IJN $.
+
   $( Substitution of equal classes into elementhood relation.  (Contributed by
      Peter Mazsa, 17-Jul-2019.) $)
   eqelb $p |- ( ( A = B /\ A e. C ) <-> ( A = B /\ B e. C ) ) $=
@@ -550579,6 +550591,12 @@ A collection of theorems for commuting equalities (or
     ( cv wcel wi wal wa wral pm5.42 albii df-ral 3bitr4ri ) CEDFZABGZ
     GZCHOAOBIGZGZCHPCDJRCDJQSCOABKLPCDMRCDMN $.
 
+  $( (Contributed by Peter Mazsa, 20-Jun-2024.) $)
+  alim2 $p |- ( A. x ( ph -> ( x e. A -> ps ) ) <->
+                A. x e. A ( ph -> ps ) ) $=
+    ( wi wral cv wcel wal df-ral bi2.04 albii bitr2i ) ABEZCDFCGDHZNE
+    ZCIAOBEEZCINCDJPQCOABKLM $.
+
   $( (Contributed by Peter Mazsa, 13-May-2024.) $)
   2imnang $p |- ( A. x A. y ( ph -> -. ps ) <-> A. x A. y -. ( ph /\ ps ) ) $=
     ( wn wi wal wa imnang albii ) ABEFDGABHEDGCABDIJ $.
@@ -550592,6 +550610,15 @@ A collection of theorems for commuting equalities (or
     IJZPKCLBLQAJFCLBLPBCDEMQABCNO $.
   $}
 
+  ${
+    $d A y $. $d x y $.
+    $( (Contributed by Peter Mazsa, 17-Jun-2020.) $)
+    r2alan $p |- ( A. x A. y ( ( ( x e. A /\ y e. B ) /\ ph ) -> ps ) <->
+                   A. x e. A A. y e. B ( ph -> ps ) ) $=
+      ( cv wcel wa wi wal wral impexp 2albii r2al bitr4i ) CGEHDGFHIZAI
+    BJZDKCKQABJZJZDKCKSDFLCELRTCDQABMNSCDEFOP $.
+  $}
+
   ${
     $d A y $. $d B x $. $d x y $.
     $( (Contributed by Peter Mazsa, 29-May-2019.) $)
@@ -550712,6 +550739,20 @@ A collection of theorems for commuting equalities (or
       IUJ $.
   $}
 
+  ${
+    a0orb.1 $e |- ( ph -> F/ x ps ) $.
+    a0orb.2 $e |- ( ph -> A = { x | ( ps /\ ch ) } ) $.
+    a0orb.3 $e |- ( ph -> B = { x | ch } ) $.
+    $( (Contributed by Peter Mazsa, 14-Jun-2024.) $)
+    a0orb $p |- ( ph -> ( A = B \/ A = (/) ) ) $=
+      ( wceq c0 wo cab cin cvv wa sylib ineq12 ancoms eqeq2i wnf inv1
+      eqcomd dfnf5 jca orim12dan syl ineqcomi 0in orbi12i inab eqeq1d
+      syl6eqr orbi12d mpbird ) AEFJZEKJZLBDMZCDMZNZFJZUTKJZLZAUTOFNZJ
+      ZUTKFNZJZLZVCAUSFJZUROJZURKJZLZPVHAVIVLAFUSIUCABDUAVLGBDUDQUEVI
+      VJVEVKVGVJVIVEUROUSFRSVKVIVGURKUSFRSUFUGVEVAVGVBVDFUTFOFFUBUHTV
+      FKUTFUITUJQAUPVAUQVBAEUTFAEBCPDMUTHBCDUKUMZULAEUTKVMULUNUO $.
+  $}
+
   ${
     $d A x y $.  $d B x y $. $d ps x $. $d ch y $.
     ceqsex2gv.3 $e |- ( x = A -> ( ph <-> ps ) ) $.
@@ -550863,18 +550904,6 @@ A collection of theorems for commuting equalities (or
     UAUBUMUTBLPBUMUSLBUMUMDUHUSLUCUMDUDUMDUEUIUFBUJUGUKUL $.
   $}
 
-  ${
-    $d A u x $.
-    $( (Contributed by Peter Mazsa, 13-Jun-2024.) $)
-    n0xpdmqs $p |- ( A =/= (/) ->
-                     ( dom ( A X. A ) /. ( A X. A ) ) = { A } ) $=
-      ( vu vx c0 wne cv cxp cec wceq cdm wrex cab cqs dmxp rexeqdv wcel
-    csn ecxpg eqeq2d rexbiia syl6bb bitr4d abbidv df-qs df-sn 3eqtr4g
-    r19.9rzv ) ADEZBFZCFZAAGZHZIZCUKJZKZBLUIAIZBLUNUKMAQUHUOUPBUHUOUP
-    CAKZUPUHUOUMCAKUQUHUMCUNAAANOUMUPCAUJAPULAUIAAUJRSTUAUPCAUGUBUCCB
-    UNUKUDBAUEUF $.
-  $}
-
   $( Restricted converse epsilon binary relation.  (Contributed by Peter Mazsa,
      10-Feb-2018.) $)
   brcnvepres $p |- ( ( B e. V /\ C e. W ) ->
@@ -551243,6 +551272,36 @@ A collection of theorems for commuting equalities (or
   rncnv $p |- ran `' A = dom A $=
     ( cdm ccnv crn dfdm4 eqcomi ) ABACDAEF $.
 
+  $( Double union of a relation.  (Contributed by Peter Mazsa, 20-Jun-2024.) $)
+  relfld2 $p |- ( Rel R -> U. U. R = dom ( R u. `' R ) ) $=
+    ( wrel cuni cdm crn ccnv relfld df-rn uneq2i dmun eqtr4i syl6eq
+    cun ) ABACCADZAEZMZAAFZMDZAGPNQDZMROSNAHIAQJKL $.
+
+  $( Range of the union of a relation with its converse.  (Contributed by
+     Peter Mazsa, 20-Jun-2024.) $)
+  rnuncnv $p  |- ( Rel R -> ran ( R u. `' R ) = dom ( R u. `' R ) ) $=
+    ( wrel ccnv cun crn df-rn cnvun dfrel2 biimpi uneq2d uncom syl6eq
+    cdm wceq syl5eq dmeqd ) ABZAACZDZESCZMSMSFQTSQTRRCZDZSARGQUBRADSQ
+    UAARQUAANAHIJRAKLOPO $.
+
+  $( Double union of a relation.  (Contributed by Peter Mazsa, 20-Jun-2024.) $)
+  relfld3 $p |- ( Rel R -> U. U. R = ran ( R u. `' R ) ) $=
+    ( wrel cuni ccnv cun cdm crn relfld2 rnuncnv eqtr4d ) ABACCAADEZF
+    KGAHAIJ $.
+
+  ${
+    $d R x y $.
+    $( Two ways of saying that a relation is strictly complete.  (Contributed
+       by Peter Mazsa, 19-Jun-2024.) $)
+    scompl $p  |- ( Rel R ->
+        ( ( dom ( R u. `' R ) X. ran ( R u. `' R ) ) C_ ( R u. `' R ) <->
+          A. x e. U. U. R A. y e. U. U. R ( x R y \/ y R x ) ) ) $=
+      ( wrel cv wbr wo cuni wral ccnv cun crn cdm cxp relfld2 relfld3
+      wss raleqdv raleqbidv qfto syl6rbbr ) CDZAEZBEZCFUDUCCFGZBCHHZI
+      ZAUFIUEBCCJKZLZIZAUHMZIUKUINUHQUBUGUJAUFUKCOUBUEBUFUICPRSABUKUI
+      CTUA $.
+  $}
+
   ${
     $d R x $.
     $( Alternate definition of domain.  (Contributed by Peter Mazsa,
@@ -551501,6 +551560,17 @@ A collection of theorems for commuting equalities (or
   cnvxpdif $p |- `' ( ( A X. B ) \ C ) = ( ( B X. A ) \ `' C ) $=
     ( cxp cdif ccnv cnvdif cnvxp difeq1i eqtri ) ABDZCEFKFZCFZEBADZME
     KCGLNMABHIJ $.
+  
+    ${
+    $d A x y $. $d B x y $. $d C x y $.
+    $( Cartesian product is a subset.  (Contributed by Peter Mazsa,
+       15-Apr-2023.) $)
+    xpss3 $p |- ( ( A X. B ) C_ C <-> A. x e. A A. y e. B x C y ) $=
+      ( cv cxp wbr wi wal wcel wa wral brxp imbi1i 2albii wrel wb relxp
+    wss ssrel3 ax-mp r2al 3bitr4i ) AFZBFZCDGZHZUEUFEHZIZBJAJZUECKUFD
+    KLZUIIZBJAJUGETZUIBDMACMUJUMABUHULUIUEUFCDNOPUGQUNUKRCDSABUGEUAUB
+    UIABCDUCUD $.
+  $}
 
   $( (Contributed by Peter Mazsa, 9-Jan-2024.) $)
   rnxpdmrndif $p |- ran ( ( dom R X. ran R ) \ R ) C_ ran R $=
@@ -551861,6 +551931,11 @@ relation with an intersection with the same Cartesian product (see also
   nel02 $p |- ( A = (/) -> -. B e. A ) $=
     ( c0 wceq wcel noel eleq2 mtbiri ) ACDBAEBCEBFACBGH $.
 
+  $( The Cartesian product with the empty set is empty.  (Contributed by Peter
+     Mazsa, 15-Jun-2024.) $)
+  0xp2 $p |- ( A = (/) -> ( A X. B ) = (/) ) $=
+    ( c0 wceq cxp xpeq1 0xp syl6eq ) ACDABECBECACBFBGH $.
+
   $( Binary relationship of disjoint classes.  (Contributed by Peter Mazsa,
      9-Apr-2024.) $)
   disjbr $p |- ( ( A i^i B ) = (/) -> -. ( C A D /\ C B D ) ) $=
@@ -552084,6 +552159,47 @@ relation with an intersection with the same Cartesian product (see also
     UJUFUKUGUEUIAUEUIAIAJKZLUEUIAUQMNOPUNUIBHZUEUPUHCUICUNURQUFUGRAUH
     SUIBTUDUEUIABUQUAUBUC $.
 
+  $( A special case where a mixture of and and or appears to conform to a mixed
+     associative law.  (Contributed by Richard Penner, 26-Feb-2020.) $)
+  rp-fakeanorassTEMP $p |- ( ( ch -> ph ) <->
+                         ( ( ( ph /\ ps ) \/ ch )
+                           <-> ( ph /\ ( ps \/ ch ) ) ) ) $=
+    ( wi wo wa wb wn pm1.4 ord pm4.83 biimpi sylan2 anim1d orc anim1i jctir olc
+    ex jca simpl imim12i adantr impbii dfbi2 ordir bicomi bibi1i 3bitr2i ) CADZ
+    ACEZBCEZFZAULFZDZUNUMDZFZUMUNGABFCEZUNGUJUQUJUOUPUJUKAULUJUKAUKUJCHADZAUKCA
+    ACIJUJUSFACAKLMSNAUKULACOPQUOUJUPCUMUNACUKULCARCBRTAULUAUBUCUDUMUNUEUMURUNU
+    RUMABCUFUGUHUI $.
+
+  ${
+    $d x A $.  $d x B $.  $d x C $.
+    $( A special case where a mixture of intersection and union appears to
+       conform to a mixed associative law.  (Contributed by Richard Penner,
+       26-Feb-2020.) $)
+    rp-fakeinunassTEMP $p |- ( C C_ A <->
+                           ( ( A i^i B ) u. C ) = ( A i^i ( B u. C ) ) ) $=
+      ( vx cv wcel wi wal wa wo wss cin cun wceq rp-fakeanorassTEMP albii elun elin
+      wb bitri dfss2 dfcleq orbi1i anbi2i bibi12i 3bitr4i ) DEZCFZUGAFZGZDHUIUG
+      BFZIZUHJZUIUKUHJZIZSZDHZCAKABLZCMZABCMZLZNZUJUPDUIUKUHOPDCAUAVBUGUSFZUGVA
+      FZSZDHUQDUSVAUBVEUPDVCUMVDUOVCUGURFZUHJUMUGURCQVFULUHUGABRUCTVDUIUGUTFZIU
+      OUGAUTRVGUNUIUGBCQUDTUEPTUF $.
+  $}
+
+  $( A special case where a mixture of union and intersection appears to
+     conform to a mixed associative law.  (Contributed by Richard Penner,
+     29-Feb-2020.) $)
+  rp-fakeuninassTEMP $p |- ( A C_ C <->
+                         ( ( A u. B ) i^i C ) = ( A u. ( B i^i C ) ) ) $=
+    ( wss cin wceq rp-fakeinunassTEMP eqcom incom uncom ineq1i eqtri uneq2i eqeq12i
+    cun 3bitri ) ACDCBEZAOZCBAOZEZFTRFABOZCEZABCEZOZFCBAGRTHTUBRUDTSCEUBCSISUAC
+    BAJKLRAQOUDQAJQUCACBIMLNP $.
+
+  $( (Contributed by Peter Mazsa, 20-Jun-2024.) $)
+  uniinxpdmrn $p |- ( Rel R ->
+                      ( R u. ( S i^i ( dom R X. ran R ) ) ) =
+                      ( ( R u. S ) i^i ( dom R X. ran R ) ) ) $=
+    ( wrel cun cdm crn cxp wceq relssdmrn rp-fakeuninassTEMP sylib eqcomd
+    cin wss ) ACZABDAEAFGZMZABPMDZOAPNQRHAIABPJKL $.
+
   $( A condition equivalent to the subrelation of a complement relation.
      (Contributed by Peter Mazsa, 28-Mar-2023.) $)
   relssvvdif $p |- ( Rel A ->
@@ -552480,6 +552596,17 @@ relation with an intersection with the same Cartesian product (see also
     FUBBAFDGZUDIZUJUFUBUKUDFZFULUEUMUBUCUKUDABDJKLUBUKUDMNBACDOPUJBUGFZDGUHUIUN
     DBACMQBUGDRPSUBUEUHTUA $.
 
+  ${
+    $d A a $.
+    $( Restriction to singleton is disjoint, see also ~ disjressn2 .
+       (Contributed by Peter Mazsa, 17-Jun-2024.) $)
+    disjressn2 $p |- A. u E* a a ( R |` { A } ) u $=
+      ( cv csn cres wbr wmo wal wrmo rmosn ax-gen wcel wa cvv brres elv
+    wb mobii df-rmo bitr4i albii mpbir ) DEZAEZCBFZGHZDIZAJUEUFCHZDUG
+    KZAJUKAUJDBLMUIUKAUIUEUGNUJOZDIUKUHULDUHULSAUGUEUFCPQRTUJDUGUAUBU
+    CUD $.
+  $}
+
   ${
     brabidga.1 $e |- R = { <. x , y >. | ph } $.
     $( The law of concretion for a binary relation.  Special case of ~ brabga .
@@ -553640,7 +553767,7 @@ relation with an intersection with the same Cartesian product (see also
     $( Binary relation over a range Cartesian product, special case.
        (Contributed by Peter Mazsa, 8-Apr-2024.) $)
     brxrncnvepres $p |- ( B e. V -> ( B ( R |X. ( `' _E |` A ) ) C <->
-        ( B e. A /\  E. x E. y e. B ( C = <. x , y >. /\ B R x ) ) ) ) $=
+        ( B e. A /\ E. x E. y e. B ( C = <. x , y >. /\ B R x ) ) ) ) $=
       ( cep ccnv cres cxrn wbr wcel cv cop wceq wa wrex wex wrel xrnrel
     wb relbrcnvg ax-mp brcnvxrncnvepres2 syl5bbr ) DEFHICJZKZLZEDUHIL
     ZDGMDCMEANZBNOPDUKFLQBDRASQUHTUJUIUBFUGUAEDUHUCUDABCEDFGUEUF $.
@@ -554415,10 +554542,10 @@ range of a range Cartesian product ( ~ dfcoss4 ), but neither of these
     $d A y $.  $d B y $.  $d R y $.
     $( (Contributed by Peter Mazsa, 12-Jun-2024.) $)
     eldmressnALTV $p |- ( B e. V ->
-        ( B e. dom ( R |` { A } ) <-> ( B = A /\ B e. dom R ) ) ) $=
-      ( vy wcel csn cres cdm cv wbr wex wceq eldmres elsng eldmg bicomd
-    wa anbi12d bitrd ) BDFZBCAGZHIFBUBFZBEJCKELZRBAMZBCIFZREUBBCDNUAU
-    CUEUDUFBADOUAUFUDEBCDPQST $.
+        ( B e. dom ( R |` { A } ) <-> ( B = A /\ A e. dom R ) ) ) $=
+      ( vy wcel csn cres cdm wceq wa wbr wex eldmres elsng eldmg bicomd
+    cv anbi12d bitrd eqelb syl6bb ) BDFZBCAGZHIFZBAJZBCIZFZKZUFAUGFKU
+    CUEBUDFZBERCLEMZKUIEUDBCDNUCUJUFUKUHBADOUCUHUKEBCDPQSTBAUGUAUB $.
   $}
 
   ${
@@ -554463,23 +554590,54 @@ range of a range Cartesian product ( ~ dfcoss4 ), but neither of these
     wbr ) BEGZCFGZHZBCDAIZJSZBUCGZBCDSZHZBAKZUFHUAUDUGLTUCBCDFMNUBUEU
     HUFTUEUHLUABAEOPQR $.
 
+  $( (Contributed by Peter Mazsa, 14-Jun-2024.) $)
+  elecressn $p |- ( ( B e. V /\ C e. W ) ->
+                    ( C e. [ B ] ( R |` { A } ) <-> ( B = A /\ B R C ) ) ) $=
+    ( wcel wa csn cres cec wbr wceq elecALTV brressn bitrd ) BEGCFGHC
+    BDAIJZKGBCQLBAMBCDLHBCQEFNABCDEFOP $.
+
+  ${
+    $d A a u $.  $d R a u $.
+    $( A class ' R ' restricted to the singleton of the class ' A ' is the
+       ordered pair class abstraction of the class ' A ' and the sets in
+       relation ' R ' with ' A ' (and not in relation with the singleton
+       ' { A } ' ).
+       
+       For example, if
+       ' ( dom ( R |X. ( `' _E |` { A } ) ) /. ( R |X. ( `' _E |` { A } ) ) )
+       = { A } ' , then the quotient set (not the singleton of the quotient
+       set) and the coset elements of the quotient set are in relation
+       ' ( R |X. ( `' _E |` { A } ) ) ' , cf. ~ eceldmqs3 . That means that
+       we can use this restriction to characterize the relation between the
+       quotient set and its elements. (Contributed by Peter Mazsa,
+       16-Jun-2024.) $)
+    ressn2 $p |- ( R |` { A } ) = { <. a , u >. | ( a = A /\ A R u ) } $=
+      ( csn cres cv wcel wbr wa copab wceq dfres2 wb elsng anbi1i eqbrb
+    cvv elv bitri opabbii eqtri ) CBEZFDGZUCHZUDAGZCIZJZDAKUDBLZBUFCI
+    JZDAKDAUCCMUHUJDAUHUIUGJUJUEUIUGUEUINDUDBROSPUDBUFCQTUAUB $.
+  $}
+
   ${
     $d A x $.  $d V x $.
-    $( (Contributed by Peter Mazsa, 12-Jun-2024.) $)
+    $( Any class ' R ' restricted to the singleton of the set ' A ' (see
+       ~ ressn2 ) is reflexive, see also ~ refrelressn .  (Contributed by Peter
+       Mazsa, 12-Jun-2024.) $)
     refressn $p |- ( A e. V ->
         A. x e. ( dom ( R |` { A } ) i^i ran ( R |` { A } ) )
           x ( R |` { A } ) x ) $=
-      ( wcel cv csn cres wbr cdm crn cin wceq wa wi wb cvv adantr sylbi
-    elin eldmressnALTV elv simplbi a1i elvd biimpd adantld syl5bi imp
-    elrnressn eqcomd breq1 syl adantl mpbid jcad brressn el2v syl6ibr
-    ex ralrimiv ) BDEZAFZVCCBGHZIZAVDJZVDKZLZVBVCVHEZVCBMZVCVCCIZNZVE
-    VBVIVJVKVIVJOVBVIVCVFEZVCVGEZNZVJVCVFVGTZVMVJVNVMVJVCCJEZVMVJVQNP
-    ABVCCQUAUBUCZRSUDVBVIVKVBVINBVCCIZVKVBVIVSVIVOVBVSVPVBVNVSVMVBVNV
-    SVBVNVSPABVCCDQUJUEUFUGUHUIVIVSVKPZVBVIVOVTVPVMVTVNVMBVCMVTVMVCBV
-    RUKBVCVCCULUMRSUNUOUTUPVEVLPAABVCVCCQQUQURUSVA $.
-  $}
-
-  $( (Contributed by Peter Mazsa, 11-Jun-2024.) $)
+      ( wcel cv csn cres wbr cdm crn cin wceq wa wi elin wb cvv sylbi
+      adantr eldmressnALTV elv simplbi a1i elvd biimpd adantld syl5bi
+      elrnressn imp eqcomd breq1 adantl mpbid ex jcad brressn syl6ibr
+      syl el2v ralrimiv ) BDEZAFZVCCBGHZIZAVDJZVDKZLZVBVCVHEZVCBMZVCV
+      CCIZNZVEVBVIVJVKVIVJOVBVIVCVFEZVCVGEZNZVJVCVFVGPZVMVJVNVMVJBCJE
+      ZVMVJVQNQABVCCRUAUBUCZTSUDVBVIVKVBVINBVCCIZVKVBVIVSVIVOVBVSVPVB
+      VNVSVMVBVNVSVBVNVSQABVCCDRUIUEUFUGUHUJVIVSVKQZVBVIVOVTVPVMVTVNV
+      MBVCMVTVMVCBVRUKBVCVCCULUSTSUMUNUOUPVEVLQAABVCVCCRRUQUTURVA $.
+  $}
+
+  $( Any class ' R ' restricted to the singleton of the class ' A ' (see
+     ~ ressn2 ) is antisymmetric.  (Contributed by Peter Mazsa,
+     11-Jun-2024.) $)
   antisymressn $p |-
       A. x A. y ( ( x ( R |` { A } ) y /\ y ( R |` { A } ) x ) -> x = y ) $=
     ( cv csn cres wbr wa wceq wi wb cvv brressn simplbi anim12i eqtr3
@@ -554487,17 +554645,20 @@ range of a range Cartesian product ( ~ dfcoss4 ), but neither of these
     UHUEUIUDUHUAUBDHZUDUHUJILABCUAUBDMMNROUEUIUBUADHZUEUIUKILBACUBUAD
     MMNROPUAUBCQST $.
 
-  $( For ,~ ( R |` { A } ) , transitivity is implied by ~ eqvrel1cossressn .
-     (Contributed by Peter Mazsa, 12-Jun-2024.) $)
-  trimtrressn $p |- ( A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) ->
+  $( Any class ' R ' restricted to the singleton of the class ' A ' (see
+     ~ ressn2 ) is transitive, see also ~ trrelressn .  (Contributed by
+     Peter Mazsa, 16-Jun-2024.)
+     [dferALTV2 on { A } + pet imply ( dom |` { A } ) /. |` { A } ) ) = { A } ]
+     $)
+  trressn $p |-
       A. x A. y A. z ( ( x ( R |` { A } ) y /\ y ( R |` { A } ) z ) ->
-                       x ( R |` { A } ) z ) ) $=
-    ( cv wbr wa wi wal csn cres wceq simplr simprr jca wb cvv brressn
-    el2v imim2 mpi simpll jca2rTEMP anbi12i imbi12i sylibr 2alimi alimi )
-    AFZBFZEGZUKCFZEGZHZUJUMEGZIZCJBJUJUKEDKLZGZUKUMURGZHZUJUMURGZIZCJ
-    BJAUQVCBCUQUJDMZULHZUKDMZUNHZHZVDUPHZIVCUQVHUPVDUQVHUOIVHUPIVHULU
-    NVDULVGNVEVFUNOPUOUPVHUAUBVDULVGUCUDVAVHVBVIUSVEUTVGUSVEQABDUJUKE
-    RRSTUTVGQBCDUKUMERRSTUEVBVIQACDUJUMERRSTUFUGUHUI $.
+                       x ( R |` { A } ) z ) $=
+    ( cv csn cres wbr wa wi wal wceq an3 eqbrb anbi12i wb cvv brressn
+    el2v 3imtr4i imbi12i mpbir gen2 ax-gen ) AFZBFZEDGHZIZUGCFZUHIZJZ
+    UFUJUHIZKZCLBLAUNBCUNUFDMZUFUGEIJZUGDMZUGUJEIJZJZUOUFUJEIJZKUODUG
+    EIZJZUQDUJEIZJZJUOVCJUSUTUOVAUQVCNUPVBURVDUFDUGEOUGDUJEOPUFDUJEOU
+    AULUSUMUTUIUPUKURUIUPQABDUFUGERRSTUKURQBCDUGUJERRSTPUMUTQACDUFUJE
+    RRSTUBUCUDUE $.
 
   ${
     $d a A u $.  $d a A v $. $d a A w $.  $d R a $.  $d V u $.  $d V v $.
@@ -554523,10 +554684,25 @@ range of a range Cartesian product ( ~ dfcoss4 ), but neither of these
     FZSSFZDHSDZSASSIUBHUCSAJSKLSHDUDSSHMSNOPQR $.
 
   $( (Contributed by Peter Mazsa, 13-Jun-2024.) $)
-  1cossressucressn2 $p |- 
+  1cossressucressn $p |- 
       ,~ ( ( R |` ( A u. { A } ) ) |` { A } ) = ,~ ( R |` { A } ) $=
     ( csn cun cres ressucressn2 cosseqi ) BAACZDEHEBHEABFG $.
 
+  ${
+    $d A u $.  $d B u $.  $d C u $.  $d R u $.  $d W u $.  $d X u $.
+    $( (Contributed by Peter Mazsa, 14-Jun-2024.) $)
+    br1cossressucressn $p |- ( ( A e. V /\ B e. W /\ C e. X ) ->
+        ( B ( ,~ ( R |` ( A u. { A } ) ) |` { A } ) C <->
+          ( B = A /\
+            ( E. u e. A ( u R B /\ u R C ) \/ ( A R B /\ A R C ) ) ) ) ) $=
+      ( wcel w3a csn cres wbr wceq wa wrex wb 3adant1 anbi2d breq1 cun
+    ccoss cv wo brressn br1cossres anbi12d rexunsn 3ad2ant1 3bitrd )
+    BFIZCGIZDHIZJCDEBBKZUAZLUBZUNLMZCBNZCDUPMZOZURAUCZCEMZVADEMZOZAUO
+    PZOZURVDABPBCEMZBDEMZOZUDZOZULUMUQUTQUKBCDUPGHUERULUMUTVFQUKULUMO
+    USVEURAUOCDEGHUFSRUKULVFVKQUMUKVEVJURVDVIABBFVABNVBVGVCVHVABCETVA
+    BDETUGUHSUIUJ $.
+  $}
+
   ${
     $d A x $. $d B x $. $d C x $. $d R x $. $d V x $. $d W x $.
     $( (Contributed by Peter Mazsa, 31-Dec-2018.) $)
@@ -554546,24 +554722,39 @@ range of a range Cartesian product ( ~ dfcoss4 ), but neither of these
       wa wb ) DFGZAHZDEIUABHZEIRACJZBDECKLMZTUBUDGUCSBACDUBEFNOPQ $.
   $}
 
+  ${
+    $d A y $. $d B y $. $d R y $. $d W y $.
+    $( (Contributed by Peter Mazsa, 14-Jun-2024.) $)
+    ecressn $p |- ( ( A e. V /\ B e. W ) ->
+                    ( [ B ] ( R |` { A } ) = [ A ] R \/
+                      [ B ] ( R |` { A } ) = (/) ) ) $=
+      ( vy wcel wa wceq cv wbr csn cres cec nfvd cab wb cvv elecressn
+      elvd eqbrb syl6bb abbi2dv adantl dfec2 adantr a0orb ) ADGZBEGZH
+      ZBAIZAFJZCKZFBCALMNZACNZUJUKFOUIUNUKUMHZFPIUHUIUPFUNUIULUNGZUKB
+      ULCKHZUPUIUQURQFABULCERSTBAULCUAUBUCUDUHUOUMFPIUIFACDUEUFUG $.
+  $}
+
   ${
     $d A x y $. $d B x y $. $d R x y $. $d V y $. $d W x y $.
     $( (Contributed by Peter Mazsa, 1-Jun-2024.) $)
     ec1cossressn $p |- ( ( A e. V /\ B e. W ) ->
                          ( [ B ] ,~ ( R |` { A } ) = [ A ] R \/
                            [ B ] ,~ ( R |` { A } ) = (/) ) ) $=
-      ( vy vx wcel wa cec wceq c0 wo wbr cab cv cin cvv ineq12 ancoms
-    csn ccoss dfec2 eqcomd adantr ab0orv orim12dan mpan2 syl ineqcomi
-    cres inv1 eqeq2i 0in orbi12i sylib wrex ec1cossres anbi12d rexsng
-    breq1 abbidv sylan9eqr inab syl6eqr eqeq1d orbi12d mpbird ) ADHZB
-    EHZIZBCAUAZUKUBJZACJZKZVMLKZMABCNZFOZAFPZCNZFOZQZVNKZWBLKZMZVKWBR
-    VNQZKZWBLVNQZKZMZWEVKWAVNKZWJVIWKVJVIVNWAFACDUCUDUEWKVRRKZVRLKZMW
-    JVQFUFWKWLWGWMWIWLWKWGVRRWAVNSTWMWKWIVRLWAVNSTUGUHUIWGWCWIWDWFVNW
-    BVNRVNVNULUJUMWHLWBVNUNUMUOUPVKVOWCVPWDVKVMWBVNVKVMVQVTIZFOZWBVJV
-    IVMGPZBCNZWPVSCNZIZGVLUQZFOWOGFVLBCEURVIWTWNFWSWNGADWPAKWQVQWRVTW
-    PABCVAWPAVSCVAUSUTVBVCVQVTFVDVEZVFVKVMWBLXAVFVGVH $.
+      ( vy vx wcel wa wbr csn cres ccoss cec nfvd wrex cab wceq breq1
+      cv ec1cossres anbi12d rexsng abbidv sylan9eqr dfec2 adantr
+      a0orb ) ADHZBEHZIZABCJZAFTZCJZFBCAKZLMNZACNZUKULFOUJUIUPGTZBCJZ
+      URUMCJZIZGUOPZFQULUNIZFQGFUOBCEUAUIVBVCFVAVCGADURARUSULUTUNURAB
+      CSURAUMCSUBUCUDUEUIUQUNFQRUJFACDUFUGUH $.
   $}
 
+  $( (Contributed by Peter Mazsa, 14-Jun-2024.) $)
+  ecressn2 $p |- ( A e. V ->
+      ( B e. dom ( R |` { A } ) -> [ B ] ( R |` { A } ) = [ A ] R ) ) $=
+    ( wcel csn cres cdm cec wceq wa c0 wo ecressn wn wi ecdmn0 biimpi
+    wne adantl df-ne sylib orel2 syl mpd ex ) ADEZBCAFGZHZEZBUHIZACIJ
+    ZUGUJKZULUKLJZMZULABCDUINUMUNOZUOULPUMUKLSZUPUJUQUGUJUQBUHQRTUKLU
+    AUBUNULUCUDUEUF $.
+
   $( (Contributed by Peter Mazsa, 9-Jun-2024.) $)
   ec1cossressn2 $p |- ( A e. V ->
       ( B e. dom ,~ ( R |` { A } ) -> [ B ] ,~ ( R |` { A } ) = [ A ] R ) ) $=
@@ -554572,6 +554763,21 @@ range of a range Cartesian product ( ~ dfcoss4 ), but neither of these
     ZEZBUIRZACRJZUHUKKZUMULLJZMZUMABCDUJNUNUOOZUPUMPUNULLSZUQUKURUHUK
     URBUIQTUAULLUBUCUOUMUDUEUFUG $.
 
+  ${
+    $d A u x $.
+    $( erimsn cf. ~ 0nep0 . (Contributed by Peter Mazsa, 15-Jun-2024.) $)
+    n0xpdmqs $p |- 
+       ( ( A =/= (/) -> ( dom ( A X. A ) /. ( A X. A ) ) = { A } ) /\
+         ( A = (/) -> ( dom ( A X. A ) /. ( A X. A ) ) = A ) ) $=
+      ( vu vx c0 wne cxp cdm cqs csn wceq wi cec wrex dmxp rexeqdv wcel
+    cv cab ecxpg syl6eq eqeq2d rexbiia syl6bb r19.9rzv bitr4d 3eqtr4g
+    abbidv df-qs df-sn 0xp2 dmeqd dm0 qseq1d 0qs eqeq2 mpbird pm3.2i
+    ) ADEZAAFZGZUSHZAIZJKADJZVAAJZKURBQZCQZUSLZJZCUTMZBRVEAJZBRVAVBUR
+    VIVJBURVIVJCAMZVJURVIVHCAMVKURVHCUTAAANOVHVJCAVFAPVGAVEAAVFSUAUBU
+    CVJCAUDUEUGCBUTUSUHBAUIUFVCVDVADJVCVADUSHDVCUTDUSVCUTDGDVCUSDAAUJ
+    UKULTUMUSUNTADVAUOUPUQ $.
+  $}
+
   ${
     $d A u y $. $d B u y $. $d V u y $.
     $( (Contributed by Peter Mazsa, 3-Jun-2024.) $)
@@ -555097,6 +555303,32 @@ range of a range Cartesian product ( ~ dfcoss4 ), but neither of these
       HURVFVHUQVHUQRBCUMUNUPDSSUDTUEURVFRACUMUPDSSUFTUGQVDVJVFBVCULUHUIUJUK $.
   $}
 
+  ${
+    brresiALT.1 $e |- C e. _V $.
+    $( TEMP (Contributed by Peter Mazsa, 27-Feb-2019.) $)
+    brresiALT $p |- ( B ( R |` A ) C <-> ( B e. A /\ B R C ) ) $=
+      ( cvv wcel cres wbr wa wb brres ax-mp ) CFGBCDAHI
+    BAGBCDIJKEABCDFLM $.
+  $}
+
+  ${
+    $d A y $. $d x y $.
+    alresanim.1 $e |- B e. _V $.
+    alresanim.2 $e |- C e. _V $.
+    alresanim.3 $e |- D e. _V $.
+    $( TEMP (Contributed by Peter Mazsa, 20-Feb-2019.) $)
+    alresanim $p |- 
+        ( A. x A. y ( ( x ( R |` A ) B /\ y ( S |` A ) C ) ->
+                      x ( T |` A ) D ) <->
+          A. x e. A A. y e. A ( ( x R B /\ y S C ) -> x T D ) ) $=
+      ( cv cres wbr wa wi wal wcel brresiALT wral anbi12i an4 imbi12i
+      bitri anass anandi imbi2i imdistan pm5.3 3bitr4i bitr4i 2albii
+      r2al ) AMZDGCNOZBMZEHCNOZPZUOFICNOZQZBRARUOCSZUQCSZPZUODGOZUQEH
+      OZPZUOFIOZQZQZBRARVIBCUAACUAVAVJABVAVDVGPZVBVHPZQZVJUSVKUTVLUSV
+      BVEPZVCVFPZPVKUPVNURVOCUODGJTCUQEHKTUBVBVEVCVFUCUECUOFILTUDVKVD
+      VHPZQVKVDVLPZQVJVMVPVQVKVPVBVCVHPPVQVBVCVHUFVBVCVHUGUEUHVDVGVHU
+      IVDVGVLUJUKULUMVIABCCUNUL $.
+  $}
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -555607,6 +555839,15 @@ when we switch from (general) sets to relations in ~ dfrefrels2 ,
     ( ccoss wrefrel cid cdm crn cxp cin wss wrel wa refrelcoss2 dfrefrel2 mpbir
     ) ABZCDOEOFGHOIOJKALOMN $.
 
+  ${
+    $d A x $.  $d R x $.  $d V x $.
+    $( Any class ' R ' restricted to the singleton of the set ' A ' (see
+       ~ ressn2 ) is reflexive.  (Contributed by Peter Mazsa, 12-Jun-2024.) $)
+    refrelressn $p |- ( A e. V -> RefRel ( R |` { A } ) ) $=
+      ( vx wcel cv csn cres wbr cdm crn cin wral wrefrel refressn wrel
+    relres dfrefrel5 mpbiran2 sylibr ) ACEDFZUABAGZHZIDUCJUCKLMZUCNZD
+    ABCOUEUDUCPBUBQDUCRST $.
+  $}
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -555948,6 +556189,41 @@ element of the class of irreflexive relations ( ~ df-irrefrels ) is
     syl6bbr ) ABZACZDAEZAFZGZHAIZUGAJZKZUDUHUCALNDUIHMOUIDHMOZUHUJDUI
     MPDUGAQUJUKUIBUEUFARUISTUAUB $.
 
+  ${
+    $d R x $.
+    $( Alternate definition of the irreflexive relation predicate. (Contributed
+       by Peter Mazsa, 21-Jun-2024.) $)
+    dfirrefrel12 $p |- ( IrRefRel R <-> 
+                       ( A. x e. U. U. R -. x R x /\ Rel R ) ) $=
+      ( wirrefrel cv wbr wn cdm crn cun wral wrel wa dfirrefrel9 relfld
+    cuni raleqdv pm5.32ri bitr4i ) BCADZSBEFZABGBHIZJZBKZLTABOOZJZUCL
+    ABMUCUEUBUCTAUDUABNPQR $.
+  $}
+
+  ${
+    $d R x $.
+    $( Alternate definition of the irreflexive relation predicate. (Contributed
+       by Peter Mazsa, 21-Jun-2024.) $)
+    dfirrefrel14 $p |- ( IrRefRel R <-> ( { x | x R x } = (/) /\ Rel R ) ) $=
+      ( wirrefrel cv wbr wn wal wrel wa cab wceq dfirrefrel5 ab0 anbi1i
+    c0 bitr4i ) BCADZQBEZFAGZBHZIRAJOKZTIABLUASTRAMNP $.
+  $}
+
+  ${
+    $d R x $.
+    $( (Contributed by Peter Mazsa, 24-Jan-2019.) $)
+    dffix4 $p |- Fix R = { x | x R x } $=
+      ( cv cfix wcel cab wbr abid2 vex elfix abbii eqtr3i ) ACZBDZEZAFN
+    MMBGZAFANHOPAMBAIJKL $.
+  $}
+
+  $( Alternate definition of the reflexive relation predicate.  (Contributed
+     by Peter Mazsa, 21-Jun-2024.) $)
+  dfirrefrel13 $p |- ( IrRefRel R <-> ( Fix R = (/) /\ Rel R ) ) $=
+    ( wirrefrel cid cin c0 wceq wrel wa dfirrefrel4 cdm relin1 reldm0
+    cfix wb syl df-fix eqeq1i syl6bbr pm5.32ri bitri ) ABACDZEFZAGZHA
+    MZEFZUCHAIUCUBUEUCUBUAJZEFZUEUCUAGUBUGNACKUALOUDUFEAPQRST $.
+
   $( Implication of irreflexive, or irreflexive, relation.  (Contributed
      by Peter Mazsa, 29-Mar-2024.) $)
   irrefimrefrel2 $p |- ( IrRefRel R -> RefRel ( ( dom R X. ran R ) \ R ) ) $=
@@ -556105,7 +556381,7 @@ element of the class of irreflexive relations ( ~ df-irrefrels ) is
   $( Irreflexive relation implies reflexive incomparability relation.
      (Contributed by Peter Mazsa, 10-May-2024.) $)
   irrefimrefincomparel2 $p |- ( R e. V ->
-                            ( IrRefRel R -> RefRel InCompaRelTo R ) ) $=
+                                ( IrRefRel R -> RefRel InCompaRelTo R ) ) $=
     ( wcel cid cdm crn cxp cin cvv cdif wss wrel wa ccnv cun wirrefrel
     cincomparelto wrefrel irrefimrefincomparel dfirrefrel2 dfincomparelto2
     wceq wb refreleq ax-mp dfrefrel2 bitri 3imtr4g ) ABCDAEAFGHIIGZAJ
@@ -556740,6 +557016,17 @@ class of symmetric relations as well (like the elements of the class of
   trreleq $p |- ( R = S -> ( TrRel R <-> TrRel S ) ) $=
     ( wceq ccom wrel wa wtrrel coideq id sseq12d releq anbi12d dftrrel2 3bitr4g
     wss ) ABCZAADZAOZAEZFBBDZBOZBEZFAGBGPRUASUBPQTABABHPIJABKLAMBMN $.
+  
+  ${
+    $d A x y z $.  $d R x y z $.
+    $( Any class ' R ' restricted to the singleton of the class ' A ' (see
+     ~ ressn2 ) is transitive.  (Contributed by Peter Mazsa, 17-Jun-2024.) $)
+    trrelressn $p |- TrRel ( R |` { A } ) $=
+      ( vx vy vz csn cres wtrrel cv wbr wal wrel trressn relres pm3.2i
+    wa wi dftrrel3 mpbir ) BAFZGZHCIZDIZUAJUCEIZUAJPUBUDUAJQEKDKCKZUA
+    LZPUEUFCDEABMBTNOCDEUARS $.
+  $}
+
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -557902,7 +558189,7 @@ complement class of the coelements on the domain is equal to the (relative)
     IBCJZOKPDKIADELODPMN $.
 
   $( Equivalence relation on a singleton implies that the Cartesian square of
-     the element of the singleton is equal to the relation.  (Contributed by
+     the element of the singleton is equal to the relation. (Contributed by
      Peter Mazsa, 13-Jun-2024.) $)
   erimsn $p |- ( ( A e. V /\ R e. W ) ->
                  ( R ErALTV { A } -> ( A X. A ) = R ) ) $=
@@ -558605,6 +558892,22 @@ instead of simply using converse functions (cf. ~ dfdisjALTV ).
   disjALTVxrnidres $p |- Disj ( R |X. ( _I |` A ) ) $=
     ( cid wdisjALTV cres cxrn disjALTVid disjimxrnres ax-mp ) CDBCAEFDGABCHI $.
 
+  ${
+    $d A a u $.  $d R a u $.
+    $( Restriction to singleton is disjoint, cf. ~ ressn2 .  (Contributed by
+       Peter Mazsa, 17-Jun-2024.) $)
+    disjressn $p |- Disj ( R |` { A } ) $=
+      ( va vu csn cres wdisjALTV cv wbr wmo disjressn2 wrel dfdisjALTV4
+    wal relres mpbiran2 mpbir ) BAEZFZGZCHDHSICJDNZDABCKTUASLBRODCSMP
+    Q $.
+  $}
+
+$(
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+                Antisymmetry
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+$)
+
 $( (End of Peter Mazsa's mathbox.) $)