If $A$ exists and $m$ is in $A$, then $m$ exists I have a doubt.
Let us consider two statements (considered true):

*

*There is a set $A$.

*$m$ is an element of $A$.

Can we then ensure that $m$ also exists?
My question arose when reading the book Introduction to Modern Set Theory (third edition), by Judith Roitman:
Infinity Axiom: ∃x Ø ∈ x and x is inductive.
And soon after:
Proposition 28: ∃x x = Ø
(The Proposition is proved on the basis of the given Axiom)
Well... I think the Axiom already guarantees the existence of the set Ø.
I think so, but I'm very unsure about it.
 A: If you can write "$m\in A$" then you already have a term $m$, and every term refers to something, so you're already assuming something exists. The statement "$m$ exists" isn't a meaningful proposition. (An existence sentence always introduces a new symbol, as in "there exists a natural number $x$ such that $x>10$".)
A: IMO, Roitman's approach is a bit weird...
The author does not state (as usual) an Empty Set Axiom: $\exists z \forall w (w \notin z)$, but introduce only a definition: $z=\emptyset \text { iff } \forall w (w \notin z)$.
Definitions do not "create" objects; thus, based on the definition, we cannot assert that there is the empty set, but we are only authorized to use the defined symbol as an abbreviation: e.g. $x \ne \emptyset$ means "$x$ is not empty".
In order to prove that some set exists, the author uses Infinity Axiom and Separation: Separation will be used in conjunction with an already existing set $X$ to "carve out" from it the empty set with the condition: $y \ne y$.
In details, the following instance of Separation must be used:

$\exists z (w \in z \text { iff } w \in X \text  { and } (w \ne w) )$.

Due to the fact that condition $w \ne w$ is always false, there will be no $w$ that belongs to set $z$, i.e. $\forall w(w \ne z)$, i.e. $z$ is empty.
Now we may assert that there is a set that is empty; by Extensionality, if there is one it will be unique, and thus we can assert that the empty set exists.
The proof above applies Separation to the set $X$ whose existence is asserted by the Infinity Axiom: the "obscure point" is that the symbol $\emptyset$ is used in the statement of the axiom, and this seems not correct to me.
See also the post Axiom of infinity and empty set; in order to avoid circularity, we have to state Infinity Axioms as follows:

$∃X[∃z(z \in X \land ∀w(w \notin z)) \land ∀x( x \in X \to x \cup  \{ x \} \in X)]$.


In conclusion, if you want to follow Roitman's approach and avoid Empty Set Axiom, I think that it is better to avoid introducing a symbol (an individual constant) for it before having proved its existence.
A more streamlined approach will be: (i) state Infinity Axiom in the form above; (ii) use it to "feed" Separation in order to prove: $\exists z \forall w (w \notin z)$; (iii) use Extensionality to prove that two sets that are empty are equal.
Finally, having proved that there is a unique set that is empty, add to the language a new symbol for it.
A: It seems to me that, since the constant $\emptyset$ has been introduced by AOI (or other axiom),  we can infer $\emptyset = \emptyset$ by reflexivity. Therefore, we can infer by existential generalization (Intro $\exists$) that $\exists x: x=\emptyset$.
