Creating New Sets within ZF I'm beginning to read about set theory and ZF these days, and the problem concerning the existence of sets has been on my mind lately.
In naive set theory, we frequently come across illustrative examples such as 'the set of vowels := {a, e, i o, u}' or 'the set of employees in a company'. I'm still kind of new to ZF and its implications, and so I was wondering whether we can show that these sets exist within ZF.
From what I understand, it seems like apart from the axiom of infinity, all the other axioms are simply rules that tell us what we can do with sets, and none of them imply the existence of sets themselves, i.e. (not sure if my understanding is fully correct)

*

*Axiom of Extensionality states that sets are equal if they contain the same objects. That is if sets exist, which is not implied in this axiom.

*Axiom of Regularity restricts the behaviour of sets so we can't have structures where sets contain themselves. The existence of sets is not implied.

*Axiom of Specification restricts the use of set-builder notation to generating subsets from already existing sets, making unrestricted comprehension illegal and removing Russell's paradox. This only tells us we're allowed to extract elements from an existing set to create a new set, and the existence of sets is not implied.

*Axiom of Pairing states we can make another set that contains two already existing sets, but this is only when those two sets exist, and the existence of these two sets is not implied.

*Axiom of Union states we can form a set that contains all elements found in sets which are members of a set of sets (allowing us to define the usual union operation when used in tow with the Axiom of Pairing). Once again, the existence of this set of sets is not implied, it only tells us what we can do if the set exists.

*Axiom of Replacement states we can take an existing set and create a new set that contains the image of the objects of the existing set as defined by some function. Set existence is not implied.

*Axiom of Power Set states if a set exists, then we can also get another set that contains all subsets of that set. Set existence is not implied.

*Axiom of Infinity finally postulates the existence of a set, and that set is an infinite set with a certain element and a whole bunch of other elements that can be reached through a successor function. So from this we at least know one set exists.

At this point, since we know one set exists, we can create things like the empty set with the axiom of specification, and then define the natural numbers and the rest of mathematics starting from there. But then I was just thinking is it still meaningful to talk about the 'set of vowels' and a 'set of employees' just as books do in naive set theory? Do we use the axiom of replacement to generate these sets from the set whose existence is implied by the axiom of infinity?
Sorry for the long post and thanks in advance to anyone who can provide an answer. I know this is bordering on philosophy and the rest of mathematics is not quite affected by these concerns of mine, but I'm just interested to see whether experts out there actually have an opinion on this matter.
 A: In order to use ZF to carry out some kind of mathematical argument that uses the "set of vowels", we need to encode the vowels somehow, just like to carry a number theory argument we typically encode the natural numbers via the Von-Neumann representation $0:=\emptyset,$ $1:=\{\emptyset\},$ $2 := \{\emptyset,\{\emptyset\}\},$ etc.
So we might as well encode the set of all vowels as $\{0,1,2,3,4\}$ (where $0,1,2,3,4$ are abbreviations for the corresponding Von-Neumann naturals) and let $a:=0,$ $e:=1,$ etc.
Similarly with employees... at the end of the day, your argument will be something that applies to any finite set where the elements have certain relationships to each other and we can encode that in the natural numbers somehow.
The key thing here is that when we use ZF (or any other theory) to formalize some mathematical argument, there's some amount of encoding that goes on to translate between the mathematical objects named in the argument and the mathematical objects in theory ("pure" sets in the case of ZF).
(As Mjqxxxx mentions in the comments, we can weaken the axiom of extensionality so that we can have urelements, i.e. objects other than the empty set that have no elements. This is similar to how we can weaken or drop the axiom of foundation to allow sets that contain themselves. While the resulting theory is interesting for certain technical purposes, it's not really needed for formalizing mathematical arguments since, as we've seen, if we want to do an argument that naively involves objects that are not sets, we can just encode them as sets. One might argue it's more natural or easier to encode them as urelements instead, but when you get into the details, this doesn't really pan out, and e.g. Mizar - the main real-life formal proof system that actually uses set theory - opts to stick with pure sets and has other solutions for mitigating the "unnaturalness".)
