A question about intersection of system of sets

[micromass]

I disagree on the following point.

I overlooked that you are referring to: y∈{x | φ(x)} ↔ φ(y) as though it is a definition, when it is actually not.

y∈{x | φ(x)} ↔ φ(y) is a theorem of naive set theory that restates the axiom of abstraction using the {...|...} operator.

In ZF, this theorem admits Russell's paradox, and cannot be a theorem of ZF.

The correct theorem in ZF is:

y \in \{x | \phi (x) \} \Rightarrow \phi (y)

The equivalence cannot be justified from the separation axiom, and must be an implication to avoid the paradox.

And as you may probably have already guessed, and operation definition for {x | φ(x)} is required in order to eliminate {x | φ(x)} entirely to wff's in the object language:

\{x | \phi (x) \} = w \Leftrightarrow [ \forall x (x \in w \Leftrightarrow \phi (x)) \wedge w \mbox{ is a set} ] \vee [\neg \exists B \forall x (x \in B \Leftrightarrow \phi (x)) \wedge w = \emptyset]

This definition along with

\{ x | \phi (x) \} \not = \emptyset

proves the implication, but the converse


\phi (y) \Rightarrow y \in \{x | \phi (x) \}

cannot be shown to follow from separation.

Yes, I understand you completely. But I think you fail to understand me. You're taking the point-of-view of Suppes. This is not standard terminology!
Please, read another book on set theory and you will see what I'm talking about.

I can make suggestion to you that will increase your understanding and point-of-views. But only you can follow them

Good luck on your research!