The definition soundness check didn't catch an unsound definition in https://github.com/metamath/set.mm/pull/3339 even though that definition has free setvars in its definiens:
$c <> $.
wich $a wff [ x <> y ] ph $.
${
$d a b ph $. $d a b x $. $d a b y $.
df-ich $a |- ( [ x <> y ] ph <-> ( x = y \/ ( [ a / x ] [ b / y ] ph <-> [ b / x ] [ a / y ] ph ) ) ) $.
$}
I didn't try to reduce further since I can test the definition soundness check only via the CI and not locally (because of #68 and #69).
The definition soundness check didn't catch an unsound definition in https://github.com/metamath/set.mm/pull/3339 even though that definition has free setvars in its definiens:
I didn't try to reduce further since I can test the definition soundness check only via the CI and not locally (because of #68 and #69).