Given a set $X$, we write $\mathcal{P}(X)$ for the set of all subsets of $X$. This is called the powerset of $X$. Here's an example of how powersets are used. Let $X$ denote a vector space. Maybe you want to define the concept "linear subspace of $X$" in a formal way. One viewpoint is that this concept "is" the function $$f : \mathcal{P}(X) \rightarrow \{\mathrm{true},\mathrm{false}\}$$ $$f(A) \iff (...),$$ where $(...)$ is the definition of the phrase "$A$ is a subspace of $X$." So, to give the "is a subspace of" function a proper domain, you need powersets.
But, how do we know powersets even exist? Well, because its an axiom.
But you may say:
Wait, I can define the set of all subsets (the "powerset"), right? Let $X$ denote a set. Then $$\mathcal{P}(X) = \{A \mid A \subseteq X\}$$
Ergo, $\mathcal{P}(X)$ exists. So I don't need an axiom for this!
Seems convincing, right? It was Russell whom first realized that this reasoning, which is formalized by the (contradictory) axiom schema of unrestricted comprehension, is untenable. The proof goes something like this. Suppose that for any formula $\phi(x)$ I can write down, there exists a set of all $x$ satisfying $\phi(x)$. Then, there exists a set of all $x$ satisfying $x \notin x$, call it $R$. Thus $y \in R$ iff $y \notin y$, for all $y$. So $R \in R$ iff $R \notin R$, a contradiction. Basically, this happens because we cannot consistently decide whether or not $R$ should be an element of itself. See also, Russell's Paradox.
This leads to the search for new set-existence principles, which (hopefully!) don't lead to an outright contradiction like that. ZFC is one such collection of set-existence principles, perhaps the standard one, and it includes the axiom of powerset.
(By the way, I copied a large chunk of this answer from this old post of mine. I guess that makes it self-plagiarism!)
Onward.
You write:
It is said that our current basis for mathematics are the ZFC-axioms.
I agree that the current basis for mathematics is set theory. But there's more than one way of doing set theory! So I don't agree with the above statement. Here's a necessarily incomplete list:
- ZFC (Zermelo-Fraenkel set theory with choice.)
- NFU (Quine's new-foundations with urelements)
- ETCS (Lawvere's elementary theory of the category of sets.)
- SEAR (Trimble's Sets, Elements, And Relations)
- ITT (Martin-Lof Intuitionistic type theory)
Also, I reject the claim that ITT isn't a set theory. It deals with collections, and functions between collections; in my books, that makes it a set theory. And of course there's people out there like me who are unhappy with the existing approaches and are secretly at work on our own secret One Set Theory To Rule Them All. You're allowed to dream, you know :) And of course you're not forced into using any particular foundation. Invent your own, if you like (this is harder than it sounds!). But anyway, no authority figure can tell you which foundation to use.
By the way, the terms in the above list aren't just set theories, they're also distinct styles of set theory. For example, you can add various kinds of axioms positing the existence of large cardinals to ZFC, for example, and you're still doing ZFC-style set theory. The theory has changed, but the style is the same. The real challenge, from a practical formalization of math standpoint, is not to create a new set theory, its to create a new, more user-friendly style of set theory.