Is the Subset Axiom Schema in ZF necessary? I am learning the axioms of Zermelo-Fraenkel (ZF) set theory.
One axiom schema basically says that given any set S and any formula phi(x), there is a set T consisting of all those elements x of S such that phi(x). 
I find this axiom schema unsatisfying because it only guarantees that subsets of S definable by a formula are really sets.  It's like saying that a function from X to Y only exists if you can write down a formula for it rather than just allowing arbitrary single-valued subsets of X cross Y.  Is there a way in the language of ZF to say "given a set S, if T is a subset of S then T is a set?"
Related is the power set axiom.  Given a set S, there is a set P(S) consisting of exactly all the subsets of S.  But in ZF the objects of the theory are sets (no urelements).  Everything is a set.  So, the elements of P(S) are all sets.  Doesn't this mean that every subset of a given set S is a set?  If so, why the need for the subset axioms?
I can anticipate some difficulty.  I want to say that "if x is a member of P(S) then x is a set," but I cannot express the predicate "is a set" in the language of set theory, and strangely enough there is no need to since everything is a set!  I attempted:
"(for all S)(for all x)[x subset S --> (there exists y)(x = y)]"
where "x subset S" is an abbreviation for "(for all z)[z in x --> z in S]."
But this attempt is silly because when I say "for all x," x is automatically a set and there is no need to say it is a set.
I'm confused.  


*

*Are the subset axioms necessary?

*Is there a way to remove reference to a defining formula so that every subset of a given set is a set?

*If the answer to 1 is "yes" and the answer to 2 is "no" then why is set theory so weird as to allow only definable subsets on the one hand and yet allow for a set of all subsets on the other?

 A: Once upon a time, mathematicians used "naive set theory": for any logical predicate, there was a set of all objects satisfying that predicate: "unrestricted comprehension". The ability to do this was one of the main features of set theory -- the ability to gather all of the objects in a class up into a set, so that you could reason about the set.
Of course, the famous contradictions were discovered (e.g. Russell's paradox), and that put an end to naive set theory.
Now, comprehension was a rather important feature of set theory, and Zermelo kept it when he came up with his axioms for set theory. The trick was to replace unrestricted comprehension with restricted comprehension. Zermelo set theory uses a limited number of "safe" operations (e.g. pairs, power sets, unions) to build up sets, and then restricts the use of comprehension to merely selecting out elements of sets -- i.e. the axiom (scheme) of subsets -- rather than allowing it to collect elements out of the entire universe.
This turns out to be powerful enough to do mathematics, and so Zermelo set theory (and eventually ZFC) became a foundation of mathematics. 
In the very closely related NBG set theory, the axiom of subsets simply becomes "If $\Phi$ is a class, and $S$ is a set satisfying $\Phi \subseteq S$, then $\Phi$ is a set." (or there is a set with the same elements as $\Phi$, depending on technical convention)
A: So, maybe I should write this as a response. So, let's take the notions in order. First, I will reserve the word "set" for objects in the theory, and use "collection" for the more intuitive notion.
Note that "$A$ is a subset of $B$" is an abbreviation for two statements: (i) $A$ is a set; and (ii) for every $x$, if $x\in A$ then $x\in B$. So "if $A$ is a subset of $B$ then $A$ is a set" is a tautology of the form $P\wedge Q\Rightarrow P$. 
As user80 points out, you are misinterpreting the Subset Axiom schema slightly; it does not state that only those subcollections which you express as ${a\in A: \phi(a)}$ are sets (it is not an "if and only if" statement). It 'merely' states that all those are sets, leaving open that perhaps there may be "other" subcollections that may also be sets. So in your analogy, it would be like saying that if you can write down a formula for a function from $X$ to $Y$ then the result will certainly be a function, but it does not tell you that you get a function only if you can write down a formula: just that writing down a formula is a way of getting a function.
It it "necessary"? Well, it is necessary if you wish to be able to construct new sets by specifying certain elements from something that you already know to be a set. Otherwise, you'll have no warrant for saying that such objects are sets, only that they are collections. The Axiom of Separation/Subset is about one way to take a set, pare it down, and get a set.
As to the axiom of the power set, you are again misinterpreting it. It's not that the axiom of the power set says that subsets of S are sets; that's already in the notion of "subset". Rather, the Power Set Axiom tells you that you have a set whose elements are the subsets of your given set $S$. It guarantees the existence of a set which is "one level up" from $S$, in the sense that its elements are subsets of $S$. From the Axiom of Pairs and other issues it is not hard to show that if you have a finite collection of things that you know are sets, then there is a set whose elements are exactly those in your original collection (that is, it allows you to pull together those things and put them in a set). But what if you have an infinite number of things that you know are subsets of $A$? In order to make sure you have a set that contains all of them as elements, you need something beyond knowing that they are sets; that's where the Axiom of the Power Set comes in: it gives you an overset (which is a set) in which all these objects will be elements. 
How does Power Set interact with Separation/Subset? Anything you obtain using Separation will necessarily be an element of the Power Set. It does not say that those are the only things in the power set, just that those are guaranteed to be in the Power Set.
A: The subtle point you are speaking about is exactly the difference between first order logic and second order logic. In first order logic, we quantify only over objects in the universe. In second order logic, we can quantify also over subcollections of the universe. ZFC is a first order theory.
Note that the ZFC subset axiom is not saying that every subset of a set is describable in the way you mention. Rather, it is making the much milder claim that if we can describe a subset, then it is a set. And this seems totally unobjectionable.
You evidently want to consider a stronger version of the axiom, which says somehow that all the subcollections that exist anywhere are also sets. This is a second order assertion, since it is quantifying over subsets of the universe. This second order subset axiom, however, is not expressible in first order logic. The reason is that any model with an infinite set, satisfying the second-order subset axiom would have to uncountable, since it would truly contain all the subsets of its sets. Thus, there could be no countable models of your theory, which would violate the Lowenheim Skolem theorem if the axiom were expressible in first order logic. 
Nevertheless, it is natural to look into the possibilities of second order ZFC, and this is studied in set theory. It turns out that the models of your second order ZFC (using second order Replacement also) are exactly the same as the universes known as $H_\kappa$ for an inaccessible cardinal $\kappa$, one of the large cardinal notions. These models are also known as the Grothendieck universes, and are used throughout  category theory as a convenient way of formalizing the large/small distinction.
It might be a good exercise for a beginner in this area to prove that if $\kappa$ is a (strongly) inaccessible cardinal, then the collection $H_\kappa$ of sets whose transitive closure has size less than $\kappa$ is a model of second order ZFC. When $\kappa$ is inaccessible, then this universe $H_\kappa$ is the same as $V_\kappa$ in the Levy cumulative hierarchy.
Finally, let me remark that some might find it to be somewhat incoherent to propose a second-order theory as the main axiomatization of set theory. The purpose of the axiomatization, after all, is to set forth certain minimal bedrock principles that the set concept should obey, but if we make these principles second-order, then we would seem to need a prior concept of set to interpret them. That is, a second order logic only makes sense in the context of a larger set-theoretic background. So it wouldn't seem to work foundationally to provide such an axiomatization as the principal axiomatization of set theory.
