数学基礎論のイオタ表現について。前にも同じようなことを質問したのですが、ずっともやもやしています。∃!xF(x)が証明できるとき、これはF(x)を満たすxがただ一つ存在するという意味になります。そのただ一つのxをιxF(x)とかきます。このとき、F(ιxF(x))が証明できることは「定義から明らか」ということでいいんでしょうか？