Formally what is an unlabeled graph? I have no problem defining labeled graphs with set theory, but can't do the same here. My only guess is maybe you could define an unlabeled graph as the isomorphism class of all labeled graphs. Of course unless we are using something stronger then $\text{ZFC}$ this won't make any sense as we are now working with essentially a "set of all sets", even if you restrict the vertex labeling to a certain class of sets say $\mathbb{N}$ you wont be able to represent graphs of an arbitrary cardinality. Anyway if someone could give me a definition in terms of some axiomatization of set theory I'd be grateful.
 A: As Noah says, usually an unlabeled simple graph would be a set $V$ whose elements we think of as vertices, together with an irreflexive symmetric binary relation on $V$ (or alternatively a set of 2-element subsets of $V$), which tells us which vertices are connected to each other.
It looks like you're objecting that this implicitly produces a labeling for the vertices, namely whichever the elements of $V$ are.
But the point of "unlabeled" is not that we cannot possibly distinguish between the vertices, but that we decide not to care. More precisely, "unlabeled" means that when we speak about isomorphisms of graphs we're not going to demand that the isomorphism preserves the names of vertices.
This holds in particular when we speak about whether two graphs are "the same" -- which almost always implicitly means "the same up to isomorphism".
That's not particular to graphs, by the way, but is a general phenomenon for all kinds of abstract structures in mathematics. For example in group theory we may say that "there is exactly one group of order $3$", again implicitly "up to isomorphism". When we say so, we don't care that that there are many ways to realize this group, such as with addition of residue classes modulo $3$, or as composition of even permutations of $\{1,2,3\}$.
For technical reasons, speaking about entire isomorphism classes of graphs (or groups) is not in favor, because it doesn't lend itself well to formalization in ZFC set theory. In contrast, it is standard and unproblematic to have "the same" implicitly include "up to isomorphism".

By the way, typically with a labeled graph one wouldn't use the elements of $V$ directly as labels either, because one often wants to be able to apply some or all of the labels to more than one vertex.
