Shorten axpr and reduce axiom usage#5019

LegionMammal978 wants to merge 1 commit intometamath:developmetamath/set.mm:developfrom

LegionMammal978:shorten-axprLegionMammal978/set.mm:shorten-axprCopy head branch name to clipboard