How to prove that a set exists in ZFC?
With your edit, it is now clearer what you're asking -- but on the other hand you're now asking an extremely broad question that is basically the same as, "How do I prove anything in ZFC?"
Each and every axiom of ZFC -- with the exception of Extensionality and Regularity -- is there to claim that a set with certain properties exists. In order to prove that a set with whatever properties you're interested in exists, you combine those axioms into an argument and ends up with your desired conclusion. This can take ingenuity! There's no one-size-fits-all process that will allow you to go from a description of your desired set to a proof that exists without having to think and be clever along the way.
I have constructed a set, e.g. $\{\{v_0\},\{v_0,v_1\}\}$. How to prove that it exists?
This is still a bit of a strange question, because usually saying that you have "constructed" something is exactly the same as saying that you have found a combination of the set existence axioms that lead to the conclusion that it exists. Speaking about "constructing" things is a more vivid way of saying it, but what you actually do is no different from putting together an existence proof.
To be concrete, if we assume that you already have $v_0$ and $v_1$:
Apply the Axiom of Pairing to $v_0$ and $v_0$ itself. This tells you that there exists a set whose members are exactly every $y$ that equals $v_0$ or equals $v_0$. By convention, this is the set we notate $\{v_0\}$ -- so the axiom says it exists!
Apply the Axiom of Pairing again, now to $v_0$ and $v_1$. It tells you that there exists a set whose members are exactly $v_0$ and $v_1$. In other words the notation $\{v_0,v_1\}$ describes something that exists.
Apply the Axiom of Pairing a third time, now to the sets $\{v_0\}$ and $\{v_0,v_1\}$ that we constructed just previously. Again, you conclude that a set whose members are precisely $\{v_0\}$ and $\{v_0,v_1\}$ exists. Which was what we set out to prove.
(To moderate the above claim a bit, for the nitpickers: Sometimes to "construct" something is taken to mean proving that it exists using a particularly restricted set of tools, i.e. no use of the Axiom of Choice and no use of the logical Law of the Excluded Middle. However, it is more common to use the adjective "constructive" for this restricted meaning, and still let the verb "construct" be used for every straightforward direct existence proof).
The axiom of infinity explicitly states that there exists a set. In fact, it states there are two sets, at least, the empty set and the infinite set the axiom guarantees to exist.
Details may depend on the exact formulation of your $\sf ZFC$ axioms, but for your concrete example $\{\{a\},\{a,b\}\}$ we have the following:
If $a$ and $b$ are sets (this must be given! So you must already know that these are sets), then the Axiom of Pairing guarantees the existence of a set having precisely $a$ and $b$ as elements. Customary, the notation $\{a,b\}$ is introduced for this set (which is unique by the Axiom of Extensionality!). Also, it is customary to write $\{a\}$ as a shorthand for $\{a,a\}$. Thus it takes us only three applications of Pairing (plus knowledge that $a,b$ are sets) to show that $\{\{a\},\{a,b\}\}$ is a set.
Whenever you construct a set, you typically use one or more axioms that guarantee such a set (provided all "input" sets exist). Typically, you can read off from the notation used, which axiom you used, because most of the axioms are specifically of a from that allows us to justify the notations we want to work with:
- $\{x\}$ and $\{x,y\}$ means you used the Axiom of Pairing (similarly for finite enumerations such as $\{x_1,x_2,x_3,x_4,x_5\}$, but these also use the Axiom of Union under the hood) and that $x,y,x_1,x_2,x_3,x_4,x_5$ are sets;
- $\mathcal P(x)$: you used the Axiom of Power Set (and that $x$ is a set);
- $\bigcup x$: you used the Axiom of Union (and that $x$ is a set)
- $x\cup y$: Axiom of Union and Axiom of Pairing (as we can define $x\cup y:=\bigcup\{x,y\}$) and that $x,y$ are sets
- $\{\,x\in y\mid \phi(x)\,\}$: Axiom Schema of Separation and that $y$ is a set
- $\{\,F(x)\mid x\in y\,\}$: Axiom Schema of Replacement and that $y$ is a set. (Note that the class(!) builder notation $\{\,x\mid \phi(x)\,\}$ is strictly speaking a no-no when constructing sets because it matches neither Separation nor Replacement and hence only gives us a class - until proven otherwise)
- $x\cap y$: Axiom Schma of Separation as we might define it as $x\cap y:=\{\,z\in x\mid z\in y\,\}$, for instance.
- $\bigcup_{i\in I}A_i$: Axiom of Union together with Axiom Schema of Replacement as we define $\bigcup_{i\in I}A_i:=\bigcup\{\,A_i\mid i\in I\,\}$, and $I$ must be a set (as well as $i\mapsto A_i$ a class function)
- $\bigcap_{i\in I} A_i$: This can be defined as $\bigcap_{i\in I} A_i:=\{\,x\in\bigcup_{i\in I}A_i\mid \forall i\in I\colon x\in A_i\,\}$, so it uses Union and Separation. However, this conveys the intended meaning only if $I$ is non-empty, and indeed the intersection makes no sense for empty $I$ in the first place (on the other hand, in contrast to union we can adjust the definition of intersection to make sense if $I$ is a proper class!)
- $\emptyset$: Interestingly the Axiom of Infinity (or possibly another axiom that grants us the existence of some set without premises) together with the Axiom Schema of Separation, for example $\emptyset :=\{\,x\in W\mid \neg(x=x)\,\}$, where $W$ is any set guaranteed to exist (the result does not depend on $W$)
- and so on (except that there is no convenient established notation for the sets guaranteed to exit by the Axiom of Choice - after all we do not have uniqueness here; also, the inductive set guaranteed to exist per Axiom of Infinity is not unique and hence has no established name, except that we can construct the smallest inductive set $$\omega:=\{\,x\in W\mid \forall y\colon \bigl((y\in\mathcal P(W)\land y\text{ inductive})\to x\in y\bigr)\,\}$$ from any such inductive set $W$).
Also note that it is not enough to say "I tried to get a contradiction with the axioms for two hours, but I didn't find any". Instead, the only way is to use the axioms and prove that your wannabe set exists. For example, can there be a set $R$ such that one of its many elements is $\{\{\emptyset\},\{\emptyset,R\}\}$? Can we arrive at a contradiction from this assumption? Well, we might try with the Axiom of Regularity: It says that $R$ should have an element that is disjoint from $R$. But that does not help us: It might well be that the very element $\{\{\emptyset\},\{\emptyset,R\}\}$ has this property - except when $R$ also has either $\{\emptyset\}$ or $\{\emptyset,R\}$ as elements, and if $\{\emptyset\}\in R$ then either this is disjoint from $R$ or we have $\emptyset\in R$ and that is clearly disjoint from $R$. So does this lack of immediate contradiction allow such $R$ to exist? - No! My example is of this form: We have sets $A,B,R$ with $A\in R$, $B\in A$, and $R\in B$. The other axioms (in particular Pairing an Union) allow us to construct the set $S=\{A,B,R\}$ (with the obvious interpretation of this notation), and this set fails to meet the Axiom of Regularity: $B\in A\cap S$, $R\in B\cap S$, $A\in R\cap S$. Thus if we assume that $\sf ZFC$ is sound, we conclude that all attempts to construct such a set $R$ will fail. (Or if someone manages to explicitly construct such a set, we should abandon $\sf ZFC$ once and for all as being contradictory - but this will not happen).
So to repeat: "Not contradicting axioms" is far from proof of existence. Consider the continuum hypothesis, which is known to be independent from the axiom of $\sf ZFC$ (any other independent statement would work just as well, and we know since Gödel that such statements exist for every useful theory). Thus we know that the existence of a set $A$ that has strictly larger cardinality than $\Bbb N$ and strictly smaller cardinality than $\Bbb R$ (i.e., $\aleph_0<|A|<2^{\aleph_0}$) does not lead to a contradiction. But we also know that the existence of a set $B$ with the property that for all sets $X$ we have $X\in B$ if and only if there exists a set $Y$ with $\aleph_0<|Y|<2^{\aleph_0}$ does not lead to a contradiction (for if the continuum hypothesis is false, $B$ is just the empty set)! The fact that neither the existence and "set-ness" of $A$ or $B$ contradicts the axioms of $\sf ZFC$ does not make either of them an actual set. For if this argument were valid, we would have to admit that both exist. But then we get a contradiction (specifically: once again with the Axiom of Regularity) because we'd find that $B\in B$.