The usual approach is to define a concept of a first order language $\mathcal{L}$. They are usually specified by the nonlogical symbols. Well-formed formulas in the language $\mathfrak{L}$ are strings of symbols of $\mathfrak{L}$ along with the logical symbols such as $($, $)$, $\wedge$, $\neg$, variables etc. You can look up in a logic textbook the inductive definition of well-formed formulas, but something like $x \wedge y$ is a well-formed formula, but $(()\neg\wedge xy \neg$ is not a well-formed formula.
A first order theory $T$ in the language $\mathfrak{L}$ is then a collection of well-formed sentences (no free variable) in the language $\mathfrak{L}$. You would then define the deduce relation $T \vdash \varphi$ to mean that there exists a proof of $\varphi$ using $T$. A proof is just a string of of sentences $\phi_1, ..., \phi_n$ such that $\phi_n = \varphi$, each $\phi_i$ is in $T$, a logical axiom of first order logic, follows from modus ponen or generalization using previous $\phi_j$, where $j < i$.
So the above is the definition of a arbitrary first order theory in an arbitrary first order language $\mathfrak{L}$. Now let $\mathfrak{L} = \{\in\}$ a first order language consisting a single binary relation. $ZFC$ is then the first order theory in the language $\mathfrak{L}$ consisting of the "eight axioms" you mentioned above. (Note that ZFC has infinitely may axioms. For example, the axiom schema of specification is actually one axiom for each formula.)
The benefit of this approach where the general definition of first order logic is developed first is that you apply this to study first order logic in general and other first order theories such that the theory of groups, rings, vector space, random graphs, etc. Also first order logic is developed in the metatheory. That is for example, a theorem of ZFC (even if it is about infinite cardinals greater than $\aleph_1$) has a finite proof in the metatheory. However, within ZFC you can formalize first order logic. Then you can consider question about whether $ZFC$ can prove it own consistency.
By taking the approach of developing first order theories in general, you also gain a certain perspective. Some people think that ZFC is something special since it can serve as a foundation for much of mathematics. Through this approach, $ZFC$ is really just another first order theory in a very simple language consisting of a single non-logical symbol. People often have a hard time grasping the idea that $ZFC$ can have different models, for instance one where the continuum hypothesis holds and one where it does not. However, almost everyone would agree that that there exists more than one model of group theory (i.e. more than one group). Sometimes it is helpful to know that results about arbitrary first order theory still apply when one is working in ZFC set theory.
Here is a model of your "finite set theory" (including Foundation) in which there is an infinite set and Power Set and Replacement fail. Let $A=\{\emptyset,\{\emptyset\},\{\{\emptyset\}\},\{\{\{\emptyset\}\}\},\dots\}$ and let $M$ be the closure of $V_\omega\cup\{A\}$ under Pairing, Union, and taking subsets (so if $X\in M$ and $Y\subseteq X$ then $Y\in M$). It is clear that $M$ satisfies all of your axioms except possibly the negation of Infinity. To prove the negation of Infinity, note that if $X\in M$, then the transitive closure of $X$ contains only finitely many elements of cardinality $>1$ (since this is true of $A$ and for every element of $V_\omega$, and is preserved by taking pairs, unions, and subsets). So $M$ cannot contain any inductive set.
However, $M$ does contain an infinite set, namely $A$. It is also clear that $M$ fails to satisfy Power Set, since $M$ contains every subset of $A$ but $\mathcal{P}(A)\not\in M$ (either by the criterion mentioned above, or by noting that every element of $M$ is countable). Replacement also fails, since the usual recursive definition of the obvious bijection $A\to\omega$ can be implemented in $M$, so Replacement would imply $\omega$ is a set.
This model does satisfy Choice in the form "if $X$ is a set of disjoint nonempty sets then there is a set that contains one element from each of them" (since $M$ contains all subsets of $\bigcup X$). It does not satisfy Choice in the form "if $X$ is a set of nonempty sets then there exists a choice function $X\to\bigcup X$", basically because it is very hard to construct functions as sets in $M$ (for instance, if $X=A\setminus\{\emptyset\}$, the unique choice function for $X$ would have infinitely many 2-element sets in its transitive closure). Probably it is possible to build a model where any reasonable form of Choice fails, but I don't know how exactly to do that at the moment.
Best Answer
The axioms tell us the allowed ways to "make"/define new sets from given sets, and here we're just given $x$. This has elements and a set like $\{y\}$ is a subset of $x$ so it is logical to use the power set axiom, and then filter out the singletons. We can use the formula
$$\phi(y):= (\exists z: z \in y) \land \left(\forall z: \forall z': ((z \in y) \land (z' \in y)) \to (z=z')\right)$$
to state that the set $y$ has exactly one element.
Then we know $\mathscr{P}(x)$ is a set and we can justify the existence of your set by the axiom of separation applied to the power set and $\phi$ from above:
$$\{\{y\}: y \in x\} = \{y \in \mathscr{P}(x) \mid \phi(y)\}$$
Alternatively for each set $y$ we can define $\{y\}$ by the pairing axiom applied to $y$ and $y$... and we know from the axiom of extentionality that $\{y\}$ is uniquely defined from $y$. So then we can apply the axiom of replacement with the "class function" $y \to \{y\}$ with domain the given set $x$ to justify that indeed $\{\{y\}: y \in x\}$ is a set as well.
Afterthought: we could also have used $$\psi(y,x) = \exists z: (z \in x) \land ( y=\{z\})$$
and separation (and also pairing, really) in the first approach. Many ways lead to Rome.