I'll try to say something about ZFC from a slightly different perspective. I'll deliberately stay away from what's covered by the Wikipedia article Zermelo–Fraenkel set theory, not because there's anything wrong with it, but because it's already there. Same goes for Qiaochu Yuan's very good answer.
To get an idea of what ZFC is and why it's important, it's helpful to consider two quite separate mathematical themes:
- The idea of a set.
- The idea of an axiom system.
This is because, well, ZFC is an axiom system for sets.
Sets
Sets are ubiquitous mathematical objects, which you know if you've been exposed to some "higher-level mathematics" as in the question details. Naively, a set is just what you think it is: a collection of objects grouped together and labeled as a thing. Many textbooks and courses start by "defining" a set like I just did, as "a collection of objects", but you're right to think that this is not quite a definition at all; it merely replaces the term you wish to define ("set") with another one synonymous with it ("collection").
Nevertheless, after seeing some examples of sets likes {apple, banana, California} or {1, 2, 3, ...} or "the set of all English words that do not describe themselves", most people get an idea of what is meant by "a set", and are happy working with them and proving things about them.
In fact, many students of mathematics and many mathematics professionals never find themselves in need of anything more formal than this, despite the fact that almost all mathematical objects we study like groups, functions, Hilbert spaces, order relations, algebraic number fields and graphs are sets with some extra structure.
To get many ideas in mathematics going, we need to be able to do stuff with sets. We need to join sets together, intersect them, consider subsets (all sets contained in a given set), and importantly - create a set as "all things satisfying some condition". If you look back at some of the proofs or definitions you've seen, you may observe this happening quite often. "Of all possible matchings of the vertices, consider the one with minimal length" may be a step in a proof, and the first thing you do here is build the set of all possible matchings. Happens all the time.
The last thing I should mention is the core of Qiaochu's answer: people quickly discovered that if you let yourself perform such operations willy nilly, especially if you imagine that it's always ok to say "The set of all foo such that bar", you get paradoxical results, which is generally regarded as a bad thing. So, they set out to define more precisely what is ok and not ok to do with sets. This leads us naturally to the next topic, the idea of axioms.
Axioms
Notice how I didn't say "they set out to define more precisely what a set is". Mathematicians generally see little need (or ability) to define what something is, opting instead to define what it does, or what you can do with it. (Hence Gowers' slogan "A mathematical object is what it does" from "Mathematics: A Very Short Introduction".)
This is what axioms are for. We introduce some objects of study, like "points" and "lines", and maybe some relationships between them, like "a point may or may not be on a line". We then declare certain things (axioms) as being true of these objects and relationships (e.g. "for any two distinct points there is a single line they both belong to"). Then, we explore the consequences of those axioms. That's the idea of the axiomatic method.
The Fano Plane has points and lines and is not afraid to use them.
Exactly what "points" and "lines" are doesn't matter one bit; you could call them "games" and "thrones" for all we care. The idea of calling them "points" and "lines" is that they are intended to model some aspect of our intuition, but this has no implication on the theory that develops as we logically explore the axioms. Keeping the intended meaning (if such exists) in mind can be helpful, but it can also be dangerously confusing.
So we have a system of axioms for rings, and for metric spaces, and for matroids, and for many other things. Those systems are not meant to model a specific object, nor any intuitive notion. They create a universe of hopefully beautiful beasts that we can revel in. Almost all mathematical objects of study are created in this way. There are many rings (each satisfying the ring axioms) and many metric spaces (each satisfying the metric space axioms) and that's good thing.
We also have systems of axioms for specific objects we do have an intuition for. For example, the Peano axioms (PA) declare certain things as true of "the natural numbers", and we certainly know what "the set of natural numbers" is supposed to mean. In fact, the Peano axioms don't capture everything that's true of the natural numbers: there are true statements that cannot be logically derived from those axioms. Consequently, the axioms don't apply just to the set of natural numbers; just like there are many rings, there are many different "models of PA" which all satisfy the Peano axioms. We don't call each of those models "A set-of-natural-numbers" because none of them is what we had intended, so in this case the abundance of objects satisfying the axioms may be seen as a bad thing.
It's a weakness of the deductive framework called "First-order logic" that we can't have an axiom system that applies precisely to the natural numbers and to nothing else besides (other frameworks, like Second-order logic, don't suffer from this particular weakness but they do suffer from others). Many people get confused by thinking that the Peano axioms "define" or "generate" the natural numbers. They can't quite do that although they do try: they declare the existence of a number, 0, and an operation ("successor" or "next number") which can be used to generate more numbers. The problem is that PA doesn't know when to stop: it easily generates all the familiar natural numbers, but it can't prevent you from throwing in non-natural numbers while still satisfying all the axioms. This is a useful analogy to keep in mind as you think about ZFC.
The axioms of ZFC set out to define the allowed operations with sets, in order to remedy the defects mentioned above about paradoxes. Among other things, they declare that certain sets exist (the empty set, and an infinite set), and they provide methods of constructing new sets from existing ones. Thus, there are universes of sets that satisfy the axioms of ZFC; but for better or worse, just like with PA, there isn't a single such universe.
There is a minimal universe [math]L[/math] of sets created by ZFC, called the Constructible universe. In contrast with PA, however, people don't tend to feel that [math]L[/math] is the real universe of sets while the others are artifacts. In fact, most people believe that L is too small to be taken seriously as the correct universe. A great article on this question is Does V Equal L? by Penelope Maddy, who writes extensively about foundational questions in the theory of sets.
This is where people start diverging philosophically: some believe that there is a "true" universe of sets and our job is to add more axioms to capture it more and more precisely; others think that this is a false belief and there are many universes-of-sets just like there are many rings, and that this is a good thing.
Be that as it may, the inevitable richness of structure forced on us by the non-uniqueness of the universe of sets means that set theory, and in particular ZFC set theory, becomes a mathematical discipline in its own right. There are things that can be proved from the axioms in ZFC, including all of the results that most mathematicians feel is "ordinary mathematics", but then there are things that cannot be deduced from ZFC, and those create a variety of fascinating alternative mathematical worlds. The most commonly studied such worlds involve "Large Cardinals", and some people - perhaps most notably Harvey Friedman - intensely study the relationship between those "exotic" objects and the most mundane entities we know, like the natural numbers.