FOM: Axioms of Substitution

[Matt Insall]

Professor Shavrukov pointed out that my substitution axioms did not do what
I said they do.  I agreed, so here is a correction of the schema.  I hope
this takes care of the difficulties:


SUBST(psi):
(forall x)(forall y)(forall z)[{[psi(x,y)&psi(x,z)] implies y=z} implies
(thereis w)(forall y){[y is in w] iff (thereis x)[(x is in w)&psi(x,y)}&{(w
is a set) iff (x is a set)}]


Dr. Matt Insall
http://www.umr.edu/~insall