Skip to content

Commit

Permalink
Commands should be closed; no comma separator. (#4536)
Browse files Browse the repository at this point in the history
  • Loading branch information
tirix authored Jan 5, 2025
1 parent 78fb45d commit 70a5768
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions set.mm
Original file line number Diff line number Diff line change
Expand Up @@ -26028,7 +26028,7 @@ the definition of class equality ( ~ df-cleq ). Its forward implication
abeq2w $p |- ( A = { x | ph } <-> A. y ( y e. A <-> ps ) ) $=
( cab wceq cv wcel wb wal dfcleq wsb df-clab sbievw bitri bibi2i albii )
EACGZHDIZEJZUATJZKZDLUBBKZDLDETMUDUEDUCBUBUCACDNBADCOABCDFPQRSQ $.
$( $j usage 'abeq2w' avoids 'df-clel' 'ax-8' 'ax-10' 'ax-11' 'ax-12' $)
$( $j usage 'abeq2w' avoids 'df-clel' 'ax-8' 'ax-10' 'ax-11' 'ax-12'; $)
$}


Expand Down Expand Up @@ -61263,7 +61263,7 @@ Definite description binder (inverted iota)
iotaval $p |- ( A. x ( ph <-> x = y ) -> ( iota x ph ) = y ) $=
( weq wb wal cab cv csn wceq cio abbi1 df-sn eqtr4di iotaval2 syl ) ABCDZ
EBFZABGZCHZIZJABKTJRSQBGUAAQBLBTMNABCOP $.
$( $j usage 'iotaval' avoids 'ax-10', 'ax-11', 'ax-12'; $)
$( $j usage 'iotaval' avoids 'ax-10' 'ax-11' 'ax-12'; $)
$}

${
Expand Down

0 comments on commit 70a5768

Please sign in to comment.