よろしくお願いします。

X≠∅かつf:X→Yが単射⇒fに左逆写像が存在する

の一般的な教科書の証明では、空でないXから適当なa∈Xを１つ選んで逆写像を構成していますが、この空でないXからaを１つ選んで行われる証明は、全体としては論理式Ψ:=(x∈X)として、∃xΨとΨ[a/x]からの帰結に対して∃除去を行っていると考えて良いですか？