（1） 9つの公理をもつ形式的体系である。
　（2） 等号をふくむ第一階述語論理を使って形式化されている。
　（3） ∈ 以外の述語を使わない。

　9つの公理については、「いざない」 を読んでください。さて、ツェルメロ の用いた 9つの公理のなかの 1つ 「置換公理」 を フレンケル が入れ替えました──その入れ替えを ツェルメロ は反対したのですが、数学者たちは フレンケル の 「置換公理」 を使うようになったので、この公理系を ツェルメロ と フレンケル の二人の名前の頭文字を使って 「ZF の公理系」 と云うことが多い。

　集合論を作った カントール は、集合の 「並び」 を苦慮していました──すなわち、「すべての集合は整列可能かどうか」 という問題です。その ソリューション として、ツェルメロ は 「選択公理」 を提示しました。「選択公理」 とは、「空でない集合のそれぞれから 1つずつ元を選んできて、並べることができる （整列可能）」 ということです。つまり、空でない集合のそれぞれから元を 1つずつ選ぶ関数 [ 選択関数 ] が存在するという公理です。

　数学の専門書によれば、「選択公理」 の証明は哲学的 ソリューション であって、数学的 ソリューション ではないので、数学者たちのなかには 「選択公理」 を認めない人たちもいるそうですが、いちぶの数学領域を除いて、現代数学は 「選択公理」 を前提にしているそうです。

　フォン・ノイマン は、記号論理を使って集合論をさらに形式化して拡張しました。そして、ベルナイス と ゲーデル が ノイマン の形式化を単純な体系に整えました。この形式的体系を （ベルナイス と ゲーデル の名前の頭文字を使って）「BG の公理系」 と云います。「BG の公理系」 では、A (u) を任意の集合論的論理式としています。A (u) の存在は 「ZF の公理系」 から得られない──分出公理 ｛ u ∈ a │ A (u) ｝ を思い出してください。｛ u ∈ a │ A (u) ｝ を前提とした 「ZF の公理系」 で扱われる集合を 「セット」 と云い、「BG の公理系」 の ｛ u │ A (u) ｝ を 「クラス」 と云います。