Meaning of "$\Leftrightarrow$" I just read (at the beginning of this Wikipedia site) that "$A \Leftrightarrow B$" means "A can be replaced in a logical proof with B". Is this interpretation of the symbol true?
(I have so far understood the symbol for equivalence ($\Leftrightarrow$) to mean that, given $A \Leftrightarrow B$, then if A is true then B is true and vice versa and, if A is false then B is false and vice versa.)
 A: The $\Leftrightarrow$ symbol usually means Logical equivalence :

In logic, two statements $p$ and $q$ are logically equivalent if they have the same "logical content". That is, if they have the same truth value in every model.

But it can also mean Logical biconditional :

the logical connective of two statements asserting "$p \text { if and only if } q$".

The two are different but strongly related concepts :

Formulas $p$ and $q$ are logically equivalent if and only if the statement $p \text { iff } q$ is a tautology.


The link with logical proof is through the so-called Substitution Theorem of logical equivalents of classical propositional logic : if two formulas are logically equivalent then they are substitutable. 
That is, if we have $A \Leftrightarrow B$, $C_A$ is a formula containing formula $A$ and $C_B$ is obtained replacing $A$ with $B$ in $C_A$, we have that if $C_A$ is provable also $C_B$ is.
See: 


*

*Stephen Cole Kleene, Mathematical logic (1967): Replacement Theorem, page 122;

*Joseph Shoenfield, Mathematical Logic (1967), Equivalence Theorem, page 34.
A: That is essentially correct, but that is not how $A \Leftrightarrow B$ is introduced into discussion.  To be brief something like what you said is usually true as a theorem, not as a definition or axiom (See link below).
Quite commonly $A \Leftrightarrow B$ is defined after the fact to be equivalent $(A \Rightarrow B) \wedge (B \Rightarrow A)$ where $C \Rightarrow D$ is read "$C$ implies $D$".  The precise details here depend on the context and which logical system you are working with.  Given a particular context you can then state and prove various theorems that allow for substitutions.
I need to tighten up my terminology here, but hopefully you get the idea.  Please see the following link for a short precise statement of an equivalence theorem:
Stanford: Introduction to logic --- Equivalence Theorem
A: $$\iff \text { means *if and only if* }$$ 
Essentially we have that:
$$A\iff B \to (A \implies B) \text { AND } (B\implies A)$$
"A if and only if B is the same as A if B and B if A"
