置換公理の読み方がわかりません
置換公理を理解しようとしています。
置換公理とは下記のような真理関数の事だと思います。
『∀x,∀y,∀z;(A(x,y)∧A(x,z)→(y=z))
→
∀a,∃b;[∀y,(y∈b ←→ ∃x∈a;A(x,y))]』
「→」は推論ではなく含意を表しています。
この真理関数の前半部分「∀x,∀y,∀z;(A(x,y)∧A(x,z)→(y=z))」は
任意の集合xに対し、条件Aを満たす(第2成分の)集合が存在すれば唯一つであり、
(存在しない時には後半部分はどうでもよい(∵自動的にこの真理関数は真となるから))
存在する場合には、後半部分も真にならねば恒真命題(即ち公理)とはならないので後半部分は真で無ければならない。とりあえず前半部分は直ぐに意味が解釈できたのですが
後半がちょっといまいち何を言っているのかわかりません。
yは前半部分でxに従って既に一意的に定まっているのですよね。ですから後半部分"∀y"と書くのはナンセンスではないのでしょうか?
それとも、前半部分のyと後半部分のyとは異なるものなのでしょうか?
それでしたら、
『∀x,∀y,∀z;(A(x,y)∧A(x,z)→(y=z))
→
∀a,∃b;[∀w,(w∈b ←→ ∃x∈a;A(x,w))]』
と書いた方が誤解が生まれないと思うのですが、、
識者の方のこの論理式の読み方をご教示賜れば幸いでございます。