公理的集合論の置換公理を「関数の像は集合である」と説明したり理解したりする人がいます。まー、そうなんですけど、ここに出てくる「関数」を普通の意味で理解すると、まったくのトンチンカンなことになります。置換公理に出てくる「関数」は、普通の関数ではないのです。
内容：
ZF集合論
現在、公理的集合論と言えばだいたいZF集合論〈ツェルメロ／フレンケル集合論〉でしょう（他の公理的集合論もありますが）。公理の個数は書き方によって変わってしまいますが、空集合の存在と選択公理を入れて10個と考えると覚えやすい気がします（両手の指の数だから）。
- 外延性の公理
- 空集合の公理
- 順序なしペアの公理
- 分出公理図式
- 合併の公理
- ベキ集合の公理
- 無限公理
- 置換公理図式
- 正則性公理
- 選択公理
これらの公理が独立というわけではありません。例えば、無限公理と分出公理図式から空集合の存在が言えるので、空集合の公理はなくてもいいです。また、空集合の公理、ベキ集合の公理、置換公理から順序なしペアの公理は出ます。空集合の公理と置換公理図式から分出公理図式が出ます。
というわけで、上記の10個の公理（公理図式含む）は冗長な公理系ですが、冗長なのが悪いわけでもないし、使い勝手が良く覚えやすいということでは、ちょうどよい設定だと思います。
ZF集合論、あるいはZFC集合論（ZF集合論＋選択公理）は、一階述語論理をベースに構築されます。一階述語論理に理論固有の関係記号〈二項述語記号〉として '$`\in`$' を入れて、上記の公理達を表現する論理式を仮定した形式理論〈formal theory〉がZF集合論です。
一階述語論理を定義する段階で、変数の集合だの論理式の集合だの、論理式にその自由変数の集合を対応させる関数だのと、さんざん集合・関数を使いまくっています。つまり、ZF集合論によって集合概念が導入されるわけではなくて、素朴集合論と一階述語論理の土台を十分に準備した後で、あらためて形式的議論をするための形式的枠組みがZF集合論です。
なので、普通に集合概念を知って使いたいだけなら、ZF集合論のお勉強は不要と言ってもいいでしょう。
誤解を解くために
前節で「ZF集合論のお勉強は不要」と言ったのですが、素朴集合論ではボンヤリしていて誤解しやすいポイントがいくつかあるので、そのような誤解を解くために、公理的集合論であるZF集合論の発想をかじってみるのはいいかも知れません。
- すべてのモノは集合である。集合以外の存在物は考えない。
- 要素というモノがあるわけではない。所属記号 '$`\in`$' の左辺を要素と呼ぶだけ。要素も集合。
- 要素を持たない集合は空集合だけ。空集合以外に要素を持たないモノ（アトム〈原子〉と呼ぶ）は存在しない。
- 関係や関数は、（ZF集合論のなかで）集合として定義する。
素朴集合論では（おそらく無意識に）アトム〈原子〉を想定していると思います。例えば、自然数はアトムだと思っている人が多いでしょうし、それ（自然数はアトム）でいいと思います。ただし、何がアトムで何がアトムでないかを決めるのは非常に難しいので、アトムは心情的な想定に過ぎないと意識しておいたほうが無難（アトム信奉者になるのは危険）です。
関係や関数やもっともっと複雑なモノでも、結局は集合に帰着できるんだ、という発想は集合一元論で単純さを持ちます。色々なモノを考えなくて済むので単純なんですが、実際に複雑なモノを集合として組み立てるのは技術的には面倒で大変です。
アトムを想定するのが悪くないのと同様、集合ではない構造物や機能体を想定するのは別にかまいません。例えば、集合圏の射としての関数は、集合とは別物だと想定するのが普通です。「集合圏の射は対象でもある」は事実ですが、それを強く意識し続ける必要はありません。
置換公理に出てくる「関数」
さて、本題の置換公理ですが、「関数の像は集合である」と一言で表現するのは間違いではありません。しかし、ZF集合論は形式理論なので、“日本語の一言”をもとに云々するわけにはいきません。置換公理（公理図式）は、一階述語論理の論理式（の集合）で書かれているので、それを見なくてはなりません。Wikipedi項目「置換公理」から書き写すと：
$`\begin{split}
& \forall w_{1},\ldots ,w_{n}. \forall A. \big(\\
& & \left(\forall x\in A. \exists !y . \phi (x,y,w_{1},\ldots ,w_{n},A) \right) \Longrightarrow \\
& & \exists B. \forall y. \left( y\in B\Leftrightarrow \exists x\in A. \phi (x,y,w_{1},\ldots ,w_{n},A) \right)\\
& \big)
\end{split}`$
普通の意味の関数は登場していません。記号 $`\phi`$ で表されるのは論理式です。この論理式が“ある種の関数”と解釈可能なのです。が、普通の関数ではありません。
$`\phi`$ は、ZF集合論の（もちろん、一階述語論理の）論理式で、$`n + 3`$ 個の自由変数を持つものです。論理式1個に対して置換公理を1個書けます。論理式は無限にあるので、置換公理は無限個の公理の集まりです。論理式でインデックスされた論理式の族〈formula-indexed family of fomulae〉を図式〈schema〉と呼ぶ*1ので、置換公理は図式です。無限個とはいいながら、インデックスとなる論理式 $`\phi`$ は可算個しかないので、置換公理図式は、可算個の論理式の族です。
今、$`\phi`$ を固定すると、ひとつの置換公理（図式の特定の事例である論理式）が生じます。論理式の一部である次の部分に注目します。
$`\quad \forall x\in A. \exists !y . \phi (x,y,w_{1},\ldots ,w_{n},A)`$
これは、パラメータ $`w_{1},\ldots ,w_{n}`$ と $`A`$ を固定すると、次のような関数的対応がある、ということです。
$`\quad A\ni x \mapsto y`$
この“関数”を $`F`$ と書くことにすると、“関数” $`F`$ のプロファイル（域と余域の仕様）は次のように書けます。
$`\quad F_{w_{1},\ldots ,w_{n}} :A \to \mathbb{V}`$
ここで、$`\mathbb{V}`$ は、ZF集合論のすべての集合からなるZF宇宙〈ZF universe〉です。ZF宇宙は集合ではありません。ZF宇宙の部分であっても、集合でない集まりがあります。集合とは限らない集まりはクラス〈class〉と呼びます。
域または余域（その両方でも）が集合であるとは限らない“関数”をクラス関数〈class function〉と呼びます。クラス関数は、ZF宇宙 $`\mathbb{V}`$ 内の関数（普通の関数）とは限りません。したがって、普通の関数とは別な取り扱いが必要なのです。
ZF集合論にクラス関数が登場するからといって、「任意のクラス関数」のような暴力的な概念を認めているわけではありません。クラス関数 $`F`$ は、記号 '$`\in`$' を入れた一階述語論理の論理式 $`\phi`$ で定義されます。「一階述語論理により」という意味で初等的〈elementary〉という言葉を使う（副詞としても使うようです）ので、$`F`$ は初等的に定義可能なクラス関数〈elementary definable class function〉だと言えます。
というわけで、置換公理に登場する“関数”は初等的に定義可能なクラス関数のことです。
置換公理
置換公理は、出現する $`n + 1`$ 個の変数達
$`\quad w_1, \cdots, w_n, A`$
は任意でいいとして、含意命題の形をしています。含意の前件（左辺）と後件（右辺）の（非形式的・内容的な）意味は次のようです。
- 前件： $`\phi(x,y, w_1, \cdots, w_n, A)`$ が、初等的に定義可能なクラス関数 $`F_{w_1, \cdots, w_n}: A \to \mathbb{V}`$ を定義する。$`x`$ は引数変数、$`y`$ は戻り値変数になる。
- 後件： 初等的に定義可能なクラス関数の像 $`F_{w_1, \cdots, w_n}[A] \subseteq \mathbb{V}`$ は集合になる。
後件のほうは存在命題として、$`B = F_{w_1, \cdots, w_n}[A]`$ である $`B`$ が（集合として）存在する、という形になっています。
Wikipedi項目「置換公理」に、「置換公理は、通常の数学におけるほとんどの定理の証明に必ずしも必要ではない。」とあるように、初等的に定義可能なクラス関数と置換公理を持ち出して云々する必要性を感じることは滅多にないでしょう。
結局、ここで話題にしたけれど、置換公理のことは忘れてしまっても困らないでしょう。困らないけど、公理的集合論に関する知識として、次の事項を心に留めておくのは無駄ではありません（役立つことがあるかも）。
- 集合ではないクラスと、普通の関数ではないクラス関数を認めている。クラス／クラス関数を（潜在的に）使っている。
- 「任意のクラス」「任意のクラス関数」は認めてない。使ってよいのは、初等的に定義可能なクラス／クラス関数だけである。
- 分出公理図式では初等的に定義可能なクラスが、置換公理図式では初等的に定義可能なクラス関数が実際に（潜在的に）使われている。
*1:diagram や figure と区別したいなら、フランス語っぽく「シェマ」と発音するといいでしょう。
