
$( Mathelia external-check experiment, 2026-09-08.
   Hand-specified correspondences, not a general MCL translator.
   No additional $a statements. $)
mathelia-abid $p |- ( x e. { x | ph } <-> ph ) $=
  wph vx abid $.
mathelia-abid-neg $p |- ( x e. { x | -. ph } <-> -. ph ) $=
  wph wn vx abid $.
mathelia-abid-and $p |- ( x e. { x | ( ph /\ ps ) } <-> ( ph /\ ps ) ) $=
  wph wps wa vx abid $.
${
  $d x A $. $d x B $.
  mathelia-ext $p |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) $=
    vx cA cB dfcleq $.
$}
${
  $d ph y $. $d ps x $. $d x y $.
  mathelia-rename.h $e |- ( x = y -> ( ph <-> ps ) ) $.
  mathelia-rename $p |- { x | ph } = { y | ps } $=
    wph wps vx vy mathelia-rename.h cbvabv $.
$}
