Rename syl6eqssr to eqsstrrdi

This is in iset.mm and set.mm
metamath · Feb 5, 2024 · 5cfb2ea · 5cfb2ea
1 parent 1a068d5
commit 5cfb2ea
Show file tree

Hide file tree

Showing 3 changed files with 80 additions and 80 deletions.
diff --git a/changes-set.txt b/changes-set.txt
@@ -110,12 +110,12 @@ proposed  syl6eleqr eleqtrrdi   compare to eleqtrri or eleqtrrd
 proposed  syl6ss    sstrdi      compare to sstri or sstrd
 proposed  syl6sseq  sseqtrdi    compare to sseqtri or sseqtrd
 proposed  syl6eqss  eqsstrdi    compare to eqsstri or eqsstrd
-proposed  syl6eqssr eqsstrrdi   compare to eqsstrri or eqsstrrd
 (Please send any comments on these proposals to the mailing list or
 make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+ 4-Feb-24 syl6eqssr eqsstrrdi   compare to eqsstrri or eqsstrrd
 29-Jan-24 ccatw2s1ccatws2 [same] revised - eliminated unnecessary antecedent
 28-Jan-24 ccat2s1fst [same]     revised - eliminated unnecessary antecedent
 28-Jan-24 ccatw2s1ass [same]    revised - eliminated unnecessary antecedent

diff --git a/iset.mm b/iset.mm
@@ -27592,11 +27592,11 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
   $}
 
   ${
-    syl6eqssr.1 $e |- ( ph -> B = A ) $.
-    syl6eqssr.2 $e |- B C_ C $.
+    eqsstrrdi.1 $e |- ( ph -> B = A ) $.
+    eqsstrrdi.2 $e |- B C_ C $.
     $( A chained subclass and equality deduction.  (Contributed by Mario
        Carneiro, 2-Jan-2017.) $)
-    syl6eqssr $p |- ( ph -> A C_ C ) $=
+    eqsstrrdi $p |- ( ph -> A C_ C ) $=
       ( eqcomd syl6eqss ) ABCDACBEGFH $.
   $}
 
@@ -49996,7 +49996,7 @@ We use their notation ("onto" under the arrow).  (Contributed by NM,
     ffvresb $p |- ( Fun F -> ( ( F |` A ) : A --> B <->
         A. x e. A ( x e. dom F /\ ( F ` x ) e. B ) ) ) $=
       ( wfun cres wf cv cdm wcel cfv wa wral fdm cin dmres inss2 adantl wfn wss
-      eqsstri syl6eqssr sselda wceq fvres ffvelrn eqeltrrd jca ralrimiva ralimi
+      eqsstri eqsstrrdi sselda wceq fvres ffvelrn eqeltrrd jca ralrimiva ralimi
       crn simpl dfss3 sylibr funfn fnssres sylanb sylan2 eleq1d syl5ibr ralimia
       simpr fnfvrnss syl2anc df-f sylanbrc ex impbid2 ) DEZBCDBFZGZAHZDIZJZVLDK
       ZCJZLZABMZVKVQABVKVLBJZLZVNVPVKBVMVLVKBVJIZVMBCVJNWABVMOVMDBPBVMQUAUBUCVT
@@ -57019,7 +57019,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and
        10-Sep-2015.) $)
     tposss $p |- ( F C_ G -> tpos F C_ tpos G ) $=
       ( vx wss cdm ccnv c0 csn cun cv cuni cmpt ccom ctpos coss1 cres wceq dmss
-      cnvss df-tpos unss1 resmpt 4syl resss syl6eqssr coss2 syl sstrd 3sstr4g )
+      cnvss df-tpos unss1 resmpt 4syl resss eqsstrrdi coss2 syl sstrd 3sstr4g )
       ABDZACAEZFZGHZIZCJHFKZLZMZBCBEZFZUMIZUOLZMZANBNUJUQBUPMZVBABUPOUJUPVADVCV
       BDUJUPVAUNPZVAUJUKURDULUSDUNUTDVDUPQABRUKURSULUSUMUACUTUNUOUBUCVAUNUDUEUP
       VABUFUGUHCATCBTUI $.
@@ -66604,7 +66604,7 @@ texts assume excluded middle (in which case the two intersection
       sbthlemi5 $p |- ( ( EXMID /\ ( dom f = A /\ ran g C_ A ) )
           -> dom H = A ) $=
         ( vy wem cv cdm wceq wss wa cdif cun cin cuni cima sbthlem1 difss sstri
-        crn sseq2 mpbiri dfss sylib uneq1d sbthlemi3 imassrn syl6eqssr sylan9eq
+        crn sseq2 mpbiri dfss sylib uneq1d sbthlemi3 imassrn eqsstrrdi sylan9eq
         uneq2d an12s cres ccnv dmeqi dmres df-rn eqcomi ineq2i uneq12i syl6reqr
         dmun eqtri 3eqtri wcel wdc wral exmidexmid ralrimivw biantrud undifdcss
         syl6rbbr adantr eqtr4d ) LEMZNZBOZFMZUFZBPZQZQZGNZDUAZBWIRZSZBWGWKWIWAT
@@ -98002,7 +98002,7 @@ Infinity and the extended real number system (cont.)
     iooval2 $p |- ( ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) =
                  { x e. RR | ( A < x /\ x < B ) } ) $=
       ( cxr wcel wa cioo co cv clt wbr crab cr iooval cin inrab2 ressxr sseqin2
-      wceq wss mpbi rabeq ax-mp eqtri elioore ssriv syl6eqssr df-ss sylib eqtrd
+      wceq wss mpbi rabeq ax-mp eqtri elioore ssriv eqsstrrdi df-ss sylib eqtrd
       syl5reqr ) BDECDEFZBCGHZBAIZJKUNCJKFZADLZUOAMLZABCNZULUQUPMOZUPUSUOADMOZL
       ZUQUOADMPUTMSZVAUQSMDTVBQMDRUAUOAUTMUBUCUDULUPMTUSUPSULUPUMMURAUMMUNBCUEU
       FUGUPMUHUIUKUJ $.
@@ -119261,7 +119261,7 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) )
       wa c0 eluzfz1 syl rspcdva adantr subidd sum0 syl6reqr oveq2 adantl syl6eq
       cv sumeq1d wi eqeq1 eqeq1d imbi12d vtoclg imp sylan oveq2d 3eqtr4d cz cfn
       fzo0 eluzel2 eluzelz fzofig syl2anc wral elfzofz fzofzp1 fsumsub eluzp1m1
-      cbvsumv fzoval fzossfz syl6eqssr sselda adantlr syldan fsum1p syl5eqr wss
+      cbvsumv fzoval fzossfz eqsstrrdi sselda adantlr syldan fsum1p syl5eqr wss
       simpr fzp1ss fsumm1 peano2zd fsumshftm ax-1cn pncan sylancl oveq1d eqtr4d
       1zzd sylan2 fsumcl eluzfz2 addcomd eqtr3d 3eqtr3d oveq12d pnpcan2d 3eqtrd
       zcnd eqtrd wo uzp1 mpjaodan ) AJIQZIJUARZCDUBRZFUCZEHUBRZQJIUDUERZUFUGSZA
@@ -131637,7 +131637,7 @@ class of all (base sets of) groups is proper.  (Contributed by Mario
   structcnvcnv $p |- ( F Struct X -> `' `' F = ( F \ { (/) } ) ) $=
     ( cstr wbr ccnv c0 csn cdif wss cin wceq wcel cvv cxp 0nelxp cnvcnv eqsstri
     wn inss2 cnvss sseli mto disjsn mpbir cnvcnvss reldisj ax-mp mpbi wrel wfun
-    wb a1i structn0fun funrel syl dfrel2 sylib difss mp2b syl6eqssr eqssd ) ABC
+    wb a1i structn0fun funrel syl dfrel2 sylib difss mp2b eqsstrrdi eqssd ) ABC
     DZAEZEZAFGZHZVDVFIZVBVDVEJFKZVGVHFVDLZRVIFMMNZLMMOVDVJFVDAVJJVJAPAVJSQUAUBV
     DFUCUDVDAIVHVGUKAUEVDVEAUFUGUHULVBVFVFEZEZVDVBVFUIZVLVFKVBVFUJVMABUMVFUNUOV
     FUPUQVFAIVKVCIVLVDIAVEURVFATVKVCTUSUTVA $.
@@ -136684,7 +136684,7 @@ F C_ ( CC X. X ) ) $=
     txss12 $p |- ( ( ( B e. V /\ D e. W ) /\ ( A C_ B /\ C C_ D ) ) ->
       ( A tX C ) C_ ( B tX D ) ) $=
       ( vx vy wcel wa wss cv cxp cmpo crn ctg cfv ctx co cvv eqid txbasex resss
-      cres resmpo syl6eqssr adantl rnss syl tgss syl2an2r wceq ssexg txval an4s
+      cres resmpo eqsstrrdi adantl rnss syl tgss syl2an2r wceq ssexg txval an4s
       syl2an ancoms adantr 3sstr4d ) BEIZDFIZJZABKZCDKZJZJZGHACGLHLMZNZOZPQZGHB
       DVGNZOZPQZACRSZBDRSZVBVLTIVEVIVLKZVJVMKGHVLBDEFVLUAZUBVFVHVKKZVPVEVRVBVEV
       HVKACMZUDVKGHBDACVGUEVKVSUCUFUGVHVKUHUIVIVLTUJUKVEVBVNVJULZVCUTVDVAVTVCUT
@@ -136696,7 +136696,7 @@ F C_ ( CC X. X ) ) $=
     txbasval $p |- ( ( R e. V /\ S e. W ) ->
       ( ( topGen ` R ) tX ( topGen ` S ) ) = ( R tX S ) ) $=
       ( vu vv vm vn vx vy wcel wa cv cxp ctg cfv cvv wss wceq ciun cmpo crn ctx
-      co eqid txbasex cres bastg resmpo syl2an resss syl6eqssr rnss syl wral wf
+      co eqid txbasex cres bastg resmpo syl2an resss eqsstrrdi rnss syl wral wf
       cuni wex eltg3 bi2anan9 exdistrv an4 xpeq12i xpiundir xpiundi a1i iuneq2i
       uniiun 3eqtri txvalex adantr ad2antrr ssel2 anim12i an4s sylan2 ralrimiva
       txopn anassrs tgiun syl2anc fveq2d 3eqtr4d eleqtrd eqeltrid xpeq12 eleq1d