Just to enlarge on Harry's answer:
Your symbol denotes one of two specified notions of implication in formal logic
$\vdash$ -the turnstile symbol denotes syntactic implication (syntactic here means related to syntax, the structure of a sentence), where the 'algebra' of the logical system in play (for example sentential calculus) allows us to 'rearrange and cancel' the stuff we know on the left into the thing we want to prove on the right.
An example might be the classic "all men are mortal $\wedge$ socrates is a man $\vdash$ socrates is mortal" ('$\wedge$' of course here just means 'and'). You can almost imagine cancelling out the 'man bit' on the left to just give the sentence on the right (although the truth may be more complex...).
$\models$ -the double turnstile, on the other hand, is not so much about algebra as meaning (formally it denotes semantic implication)- it means that any interpretation of the stuff we know on the left must have the corresponding interpretation of the thing we want to prove on the right true.
An example would be if we had an infinite set of sentences: $\Gamma$:= {"1 is lovely", "2 is lovely", ...} in which all numbers appear, and the sentence A= " the natural numbers are precisely {1,2,...}" listing all numbers. Any interpretation would give us B="all natural numbers are lovely". So $\Gamma$, A $\models$ B.
Now, the goal of any logician trying to set up a formal system is to have $\Gamma \vdash A \iff \Gamma \models A$, meaning that the 'algebra' must line up with the interpretation, and this is not something we can take as given. Take the second example above- can we be sure that algebraic operations can 'parse' those infinitely many sentences and make the simple sentence on the right?? (this is to do with a property called compactness)
The goal can be split into two distict subgoals:
Soundness: $A \vdash B \Rightarrow A \models B$
Completeness: $A \models B \Rightarrow A \vdash B$
Where the first stops you proving things that aren't true when we interpret them and the second means that everything we know to be true on interpretation, we must be able to prove.
Sentential calculus, for example, can be proved complete (and was in Godel's lesser known, but celebrated completeness theorem), but other for other systems Godel's incompleteness theorem, give us a terrible choice between the two.
In summary: The interplay of meaning and axiomatic machine mathematics, captured by the difference between $\models$ and $\vdash$, is a subtle and interesting thing.
Best Answer
You are right in your definitions, but both symbols can be used in the metatheory, meaning that they are used to describe properties and relations between objects of the theory : axioms, theorems, and between the theory and its models.
With a formal theory, like $\mathsf {ZFC}$ or $\mathsf {PA}$, based on first-order logic, it is useful to separate symbols of the language, like :
$\lnot, \rightarrow, \land, \lor$, all belonging to the common first-order language
$\in$, specific of set theory
$+$, specific of arithmetic,
and symbols used in the meta-language, like :
$\vdash$, for the relation of derivability in a theory, meaning there is a formal derivation of a theorem from the axioms of the theory
$\vDash$, for the relation of logical consequence, meaning that a sentence in the language of the theory is true in all models of the theory, i.e. in all interpretations satisfying the axioms.
The two relations are linked through Gödel's completeness theorem.
Expanded edition
The above is a précis of the "standard view", dating back to the '50s and '60s of last century; see :
See also :
And see footnote, page 36 :
See Rob's comment below ; the sequent calculus (Gentzen, 1934) is a formalization of the derivability relation. The original Gentzen's syntax for sequents :
is often written with $\vdash$ in place of the auxiliary symbol $\rightarrow$ (or sometimes : $\Longrightarrow$).