Content of $\mathbb N$ I am working with the following set of axioms:
1) There is a set.
2) Two sets are equal iff they contain equal elements.
3) if $A$ is a set and $p(x)$ is a set property (e.g. $x = x$), then $\{a \in A : p(a)\}$ is also a set.
4) if $A$ and $B$ are sets, then there is a set which contains only elements of $A$ and $B$.
5) if $\mathbb A$ a set, then $\{a | \exists A \in \mathbb A : a \in A\}$ is also a set.
6) For each set there is its power set. 
7) There is an inductive set, i.e. the one which contains $\emptyset$ and if it contains $a$, then it also contains $a^+:=a\cup\{a\}$. 
With these axioms I can prove a theorem: There is one and only one inductive set which is subset of any other inductive set. This inductive set I call $\mathbb N$ (the proof of existence is not constructive, so we do not know how $\mathbb N$ looks like).
I introduce the following notations: $0:=\emptyset,1:=0^+,2:=1^+,...$
I would like to show that $\mathbb N = \{0,1,2,3,4,...\}$, i.e. in $\mathbb N$ we have only elements "derived" from $\emptyset$.
My attempt
First of all it is not clear that $\{0,1,2,3,4,...\}$ is a set. I prove it as follows: $\{0,1,2,3,4,...\}=\{a \in \mathbb N : a = \emptyset^{+^{.^{.^{.^{+}}}}} \}$ and according to 3) $\{0,1,2,3,4,...\}$ is a set. (not sure whether this step is correct, specifically whether $a = \emptyset^{+^{.^{.^{.^{+}}}}}$ can be used as a set property). 
Then it is obvious that $\{0,1,2,3,4,...\}$ is inductive and $\subset \mathbb N$, thus $\{0,1,2,3,4,...\} = \mathbb N$ (according to the theorem).
My introduction in the set theory was rather informal, so I would also need an informal answer (a formal one I probably would not be ably to comprehend).
 A: 
I would like to show that $\mathbb N = \{0,1,2,3,4,...\}$, i.e. in $\mathbb N$ we have only elements "derived" from $\emptyset$.

Assuming that you're working in ordinary first-order logic, you cannot show that, because it is not necessarily true. More precisely, there exist models of your axiom system where there is an object that is in every inductive set, but is not one of $0,1,2,3\ldots$.
Unfortunately, the proof that such models exist is quite non-constructive, and it is not easy to display a particular model with this property. It has to exist, due to the compactness principle and Gödel's completeness theorem, but its structure is not straightforwardly describable.
Your attempt to prove that $\{0,1,2,3,\ldots\}$ is a set using the separation axiom fails because "is one of $0, 0^+, 0^{++}, \ldots$" is not something you can write down as a finite formula in the language of set theory.
One caveat, though: If you're not using first-order logic but second-order logic, you have the option of formulating the separation axiom with a formal quantification over all properties $p$ (instead of just having one instance of the axiom for each property that you can write down), then the models I'm talking about here are not actually models. You would then be able to prove as a metatheorem that in every model, every element of $\mathbb N$ has the form $0^{++\,\cdots\,++}$. (This would still not be a statement in the language of set theory, though).
However, set theory is rarely done in second-order logic, for a variety of reasons. (The most immediate one is that second-order logic is not complete: there can be sentences that are true in every model but still not provable from the axioms).
