>>419-420
> 実は別に∈以外の述語記号が現れる論理式を持ち出してもいいんですよ
> だって、結局∪とか∩とか⊂とか⊆とか使ってるじゃないですか
> それって結局∈による式で定義してるわけだけど
> 定義式込みだったらOKなわけですから

ふっふ、ほっほ
1)公理とは? 公理系とは?
 そこが根本から分ってないね
2)話は全く逆だよ
 公理や公理系を作るとき、思いっきり贅肉をそぎ落として
 使える公理を必要最小限に絞り込むんだよ!!!
3)そういう作業を、当時の数学者がみんなでして、最後に残ったのが
 下記の9つ(実は8つ)の公理だけ
 他の必要なロジックは、ここから定理として導き出される
4)お分かりか?
 もし、今のZFCで不足ならば、その不足が追加されて、9つを越える公理が定められていたんだw
5)実際、NBGの英文 wikipedia を見れば、ZFCより公理が多く複雑だ
 NBGは、”class”を導入しているので、その分公理系として複雑になる
6)公理系としては NBGは複雑にして、”class”を導入して、人間には”class”が理解しやすくなった反面
 しかし、ZFCの保存拡大だとなったらしい

 基礎論屋さんからは
「な〜んだw」ということになるww (^^;

(参考)
ja.wikipedia.org/wiki/%E3%83%84%E3%82%A7%E3%83%AB%E3%83%A1%E3%83%AD%EF%BC%9D%E3%83%95%E3%83%AC%E3%83%B3%E3%82%B1%E3%83%AB%E9%9B%86%E5%90%88%E8%AB%96
歴史的に議論を呼んだ選択公理 (AC) を含むツェルメロ=フレンケル集合論は公理的集合論の標準形式であり、今日では最も一般的な数学の基礎となっている。選択公理を含むツェルメロ=フレンケル集合論はZFCと略される

ja.wikipedia.org/wiki/%E3%83%95%E3%82%A9%E3%83%B3%E3%83%BB%E3%83%8E%E3%82%A4%E3%83%9E%E3%83%B3%EF%BC%9D%E3%83%99%E3%83%AB%E3%83%8A%E3%82%A4%E3%82%B9%EF%BC%9D%E3%82%B2%E3%83%BC%E3%83%87%E3%83%AB%E9%9B%86%E5%90%88%E8%AB%96
フォン・ノイマン=ベルナイス=ゲーデル集合論 (NBG) とはツェルメロ=フレンケル集合論+選択公理 (ZFC)の保存拡大である公理的集合論である。NBGでは、量化子の範囲を集合に限定した論理式によって定義される集合の集まりとして、クラスの概念を導入する。NBGは、すべての集合というクラスやすべての順序数というクラスといった、集合よりも大きいクラスを定義できる。モース=ケリー集合論 (MK) は量化子の範囲がクラスである論理式によるクラスの定義を許容する。NBGは有限公理化できる一方、ZFCやMKではできない。

https://en.wikipedia.org/wiki/Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory
Von Neumann–Bernays–Gödel set theory
In the foundations of mathematics, von Neumann–Bernays–Gödel set theory (NBG) is an axiomatic set theory that is a conservative extension of Zermelo–Fraenkel–choice set theory (ZFC). NBG introduces the notion of class, which is a collection of sets defined by a formula whose quantifiers range only over sets.