You've actually (perhaps unintentionally) asked a controversial question in the philosophy of logic. I don't think it's been given a lot of attention on the Phil SE, but it has definitely been danced around.
Classically, the two statements are equivalent. That's because in order for
~(x)Bx to be true, it is not the case that every x is B, which means there is some x that is not B, which means that
(∃x)~Bx. But what is the intuitive pull behind that middle equivalence?
It's actually best to go right down to the semantics of classical logic to explain this, so let's do that. In a classical model in logic, we have a collection of objects called a Domain. When we use the universal quantifier in
(x)Px, what we are doing on the classical account is we're saying "any object in the domain,
c, is such that
On this understanding, we assume that, in the language we're using to make statements like "every x is P" (as opposed to statements in our logical language like
(x)Px), we have the resources we need to go through the objects of the domain and confirm that, indeed, all of them are P. (and this seems like not a major problem, since we're restricting ourselves to talking about things in a Domain, rather than talking about "everything there is" or something like that.) We also, when push comes to shove, have the resources we need to say, of any of those objects, when they are not P. And, of course, we know that any object either is P or is not P.
So. The interpretation of why the two statements are equivalent comes together. It's because universal claims
(x)Px come out as true if, and only if, all of the objects in the domain are P. In our language where everything in the domain either is or is not P, we can tell that when not all of the objects in the domain are P (i.e.
~(x)Px is true), that must be because at least one of them is not P (for some
c in the domain,
~P(c)). And once we've established that, then we've established all we need to make
The theory of classical models of logic is probably not suited to a first course in logic, but Ch.s 9-10 of Boolos, Burgess and Jeffrey's Computability and Logic is recognised as a good overview for an intermediate-undergraduate-level audience interested in delving into the rabbit-hole of metalogic. It should be available in most universities with a mathematical logic course, and I've seen it in quite a few public libraries too.
But you're absolutely right that the latter proposition seems to have an existential commitment, where all we've done is negate a universally quantified proposition. It often seems natural to us to say that we have demonstrated that something is not universally the case without wanting to say that we have demonstrated that there is something for which the converse holds.
Constructivists in the philosophy of mathematics will want to say that this is because there is more at stake in the existential quantifier than working within an accepted domain of objects, all of which behave perfectly classically and can be safely referred to and individuated. For a constructivist, when you want to logically assert that there is something that is P, you not only make a statement about an object abstractly, but commit yourself to being able to go out and actually present the object somehow.
To explain this a little further, let's try out a mathematical technique of proving that something exists by contradiction (thanks to the wiki article on Constructive Proof for this one).
I assert that "There exist irrational numbers a and b such that a^b is rational." In defense of this claim, I ask you to consider the number
√2^√2. Either it is rational or it is irrational. If it's rational, the assertion is true. If it's irrational, however, then let that be the first irrational number a and let
√2 be the second b.
(√2^√2)^√2 = 2. So in this case, the assertion is also true, and therefore, it is always true.
You can then respond by asking me "Okay, so maybe there are such irrational numbers, but so far I'm not sure what values a and b should take for your statement to be true. Can you tell me what they might be?". And on the classical account, I am entirely within logical authority (and perhaps, if I don't know, obliged) to say "No, and I don't have to in order to have logically proven my claim."
The Constructivist will say that something is amiss wih the logic here. For a constructivist piece of reasoning to count as valid, it must in principle be possible to be able to provide examples or algorithms that serve to verify any conclusions that are drawn. This is a line that is quite common among verificationists or positivists, such as we find in abundance at the moment in a lot of popular science. That classical mathematical logic finds itself at such odds with this intuitive way of looking at what Logic is supposed to do (perhaps to reveal a conservative and transparent account of the way the world is) is something that many people find a pill too difficult to swallow.
So don't worry if the classical way of thinking about logic doesn't seem natural or intuitive. That's a recognised issue people have had with the classical idiom. The trick to getting the feel for classical logic is understanding it in well-defined contexts and in the mathematical framework for its interpretation, which might be better thought of as the problem of presenting models of collections of objects and evaluating theories of inference concerning well-defined properties about them. You can worry about where and when this kind of model is suitable for wider application once you understand how the classical standard one works.