From fb22c4b7d28a8d66449e5117079b75fea9fbc232 Mon Sep 17 00:00:00 2001 From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com> Date: Thu, 3 Oct 2024 17:33:42 +0200 Subject: [PATCH] corrections --- set.mm | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/set.mm b/set.mm index 126b11e88b..1260a50d7c 100644 --- a/set.mm +++ b/set.mm @@ -28807,7 +28807,7 @@ generally appear in a single form (either definitional, but more often rspw $p |- ( A. x e. A ph -> ( x e. A -> ph ) ) $= ( wral cv wcel wi wal df-ral weq eleq1w imbi12d spw sylbi ) ACEGCHEIZAJZC KSACELSDHEIZBJCDCDMRTABCDENFOPQ $. - $( $j usage 'rspw' avoids 'ax-8' 'df-clel' 'ax-10' 'ax-11' 'ax-12'; $) + $( $j usage 'rspw' avoids 'ax-10' 'ax-11' 'ax-12'; $) $} $( Restricted specialization. (Contributed by NM, 17-Oct-1996.) $) @@ -40066,7 +40066,7 @@ among classes ( ~ eq0 , as opposed to the weaker uniqueness among sets, FZGHUMICFZHZBJZDKZGUNUMCLUAUODUBZUNMZBNZDKZUQUOURUMMZUSNZDKVADUMUNUCVCUTD VCBUSNUTVBBUSVBACDTBADCOABCDEUDPQBUSUEPRPVAIBNZDKUQUTVDDUSIBUSICDTIIDCOIC DUFPQRVDUPDVDUPIBUPBUPUGSIJUPUHUIIBBBSBUJUKULRPPP $. - $( $j usage 'ab0' avoids 'df-clel' 'ax-8' 'ax-10' 'ax-11' 'ax-12'; $) + $( $j usage 'ab0w' avoids 'df-clel' 'ax-8' 'ax-10' 'ax-11' 'ax-12'; $) $} $( The class of sets verifying a property is the empty class if and only if