∃に関する存在定理
$ \begin{cases}P(x, f(y))\\f(y)\in A\end{cases} \iff \exist z\in A; \begin{cases}P(x, z)\\z=f(y)\end{cases}
$ Pは命題函数、$ fは函数、$ x,yは自由変項、$ Aは集合である
証明は簡単
https://kakeru.app/f3ab31a09083cd2a41423cb0d20b25df https://i.kakeru.app/f3ab31a09083cd2a41423cb0d20b25df.svg
$ \begin{aligned}\begin{cases}P(x, f(y))\\f(y)\in A\end{cases} &\iff \exist z\in A; \begin{cases}P(x, z)\\z=f(y)\end{cases}\end{aligned}