>>36
=_defが=とは別の記号なら、A =_def B は A = B とは別の式であり、
前者から後者を導き出すには公理が必要だろ？