WIP

mazsa · Jan 1, 2025 · 7c89ea6 · 7c89ea6
1 parent b8c758d
commit 7c89ea6
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/set.mm b/set.mm
@@ -581984,9 +581984,10 @@ relation with an intersection with the same Cartesian product (see also
      (Contributed by Peter Mazsa, 18-Nov-2024.)
      (Proof modification is discouraged.) $)
   mopickr $p |- ( ( E* x ps /\ E. x ( ph /\ ps ) ) -> ( ps -> ph ) ) $=
-    ( wmo wa wex wi exancom wn weu wo moeu2 bj-nexrt pm2.21 syl a1d eupickbi sp
-    wal syl6bi jaoi sylbi syl5bi imp ) BCDZABECFZBAGZUFBAECFZUEUGABCHUEBCFIZBCJ
-    ZKUHUGGZBCLUIUKUJUIUGUHUIBIUGBCMBANOPUJUHUGCSUGBACQUGCRTUAUBUCUD $.
+    ( wmo wa wex wi exancom wn weu wo moeu2 19.8a con3i pm2.21 syl a1d eupickbi
+    wal sp syl6bi jaoi sylbi syl5bi imp ) BCDZABECFZBAGZUGBAECFZUFUHABCHUFBCFZI
+    ZBCJZKUIUHGZBCLUKUMULUKUHUIUKBIUHBUJBCMNBAOPQULUIUHCSUHBACRUHCTUAUBUCUDUE
+    $.
 
   $( Sufficient condition for transitivity of conjunctions inside existential
      quantifiers.  (Contributed by Peter Mazsa, 2-Oct-2018.) $)