What is the difference between the biconditional iff. and equality = ? Hello, 
I've been used to writing logical transformations using equality, but the other day it struck me that perhaps I should be using the biconditional $\iff$?
So my question is:
What is the difference between the biconditional iff. $\iff$  and equality =  ?  Can they be used interchangeably?  And when should one be used instead of the other?  Is this matter of style?  meaning?  or correctness?
Simple Examples to illustrate the point: here p,q are propositions, ^ is "and", v is "or", and ~ is "not":
Using equality:
(1)  p ^ (q v r) = (p ^ q)  v  (p ^ r)
and
(2)  p $\Rightarrow$ q = ~ p v q
But is this more correctly written using the biconditional iff.?
(1')  p ^ (q v r) $\iff$ (p ^ q) v (p ^ r)
and
(2')  p $\Rightarrow$ q  $\iff$  ~ p v q
In rendering into English, are these logically equivalent statements?  Equal statements (equality being considered as an equivalence relation that then establishes an equivalence class)?  Or is it that the very meaning of equality in the context of logical propositions is iff.?
(Can't find the Community Wiki tag! someone please add it, thanks.)
 A: The worst problem with using equality in this way is that equality on propositions doesn't have a single meaning.  Originally, in Boole's logic, it meant that one formula was obtained from another by a series of algebraic manipulations.  Now, it might mean that the formulae belong to the same equivalence class in the Lindenbaum algebra of a logic.
The problem is that these two differ.  One might have a theory of algebraic manipulations on formulae that is decidable for a logic that is undecidable: it is not rare in proof theory to say that two formulae are equal iff they have the same negation normal form, for instance, which isan algebraic notion of equality using just De Morgan duality and that negation is involutive.  Then equality and logical equivalence do not coincide, as they must with the second interpretation.
Feel free to use equality on propositions if you wish, but do make clear what you are doing.  If you follow Amy's advice, there is no need to spell this out.
A: Usually the biconditional is denoted by $\leftrightarrow$ and logical equivalence is represented by $\Leftrightarrow$.
Given two compound propositions $P$ and $Q$, the proposition $P \Leftrightarrow Q$ means that $P$ and $Q$ have the same truth value for each possible combination of truth values of the variables of which they are composed. That is, $P \Leftrightarrow Q$ means that $P \leftrightarrow Q$ is a tautology (i.e., a proposition that is always true). It's important to note that $\leftrightarrow$ is a connective, whereas $\Leftrightarrow$ is like an "equals sign" for propositions. More formally, the expression $P \Leftrightarrow Q$ is really a proposition about a proposition, namely that "$P \leftrightarrow Q$ is a tautology", whereas the expression $P \leftrightarrow Q$ is just a compound proposition that may or may not be a tautology.
Likewise, the conditional is usually denoted by $\rightarrow$ and logical implication is represented by $\Rightarrow$. Given two compound proposition $P$ and $Q$, the proposition $P \Rightarrow Q$ means $Q$ is true whenever $P$ is true, i.e., $P \Rightarrow Q$ means that $P \rightarrow Q$ is a tautology.
It seems that you may have confused logical equivalence ($\Leftrightarrow$) with the biconditional connective ($\leftrightarrow$) and logical implication ($\Rightarrow$) with the conditional connective ($\rightarrow$).
A: Another reason to avoid conflating equality with equivalence: whether two formulas are equal should only depend on the formulas themselves. But formulas can become equivalent after some other set of axioms has been assumed, and the equivalence can depend on exactly which other axioms are assumed. 
For an elementary example in the language of rings, let $\phi$ say "there are no zero divisors" and let $\psi$ say "every element has a multiplicative inverse".  These are not the same formula, trivially. If we assume all the ring axioms and we also assume that there are no more than (say) 16 elements, the formulas become equivalent by Wedderburn's theorem. 
But if we do not assume the ring axioms, the formulas are not equivalent. For example, I could make a model with three elements {0,1,2} such that for all $x,y$ we have $xy = 2$, and this would satisfy $\phi$ but not $\psi$. Of course this is not a ring – that's the point.  Or, we could assume the ring axioms but not assume there are only a finite number of elements, and again the formulas will be inequivalent. 
(The reason for picking 16 is to avoid a technicality with first-order logic.  For each $n$ there is a sentence which says that there are no more than $n$ elements, but there is no single sentence which says there are only finitely many elements.  One can try to work around this by switching to the language of set theory, but that complicates things in other ways.)
A: In other words, $P(x)\iff Q(x)$ implies that $\forall x \in D, P(x) \leftrightarrow Q(x)$ where $D$ is the relevant domain. Or, that "$\iff$" applies when talking about logic while "$\leftrightarrow$" is used in a formula.
But to address the question as to whether $\iff$ can serve as a replacement for $=$, I think that translating it into English is useful. Replace "$\iff$" with "is necessary and sufficient for" and say "$=$" as "equals" (the same goes for "$\equiv$" and "logically equivalent to") and I think that you'll see that they are different, conceptually and syntacticly, only in certain circumstances, or "when doing logic, we speak logic" (I often use them when taking notes on non-math topics, and my brain knows what I mean regardless of symbol choice :) ).
A: If two predicates describe the same set, does that mean that they are equal or that they are logically equivalent? "$\phi = \psi$" could mean that $\phi$ and $\psi$ are literally the same formula. We write $\Leftrightarrow$ for logical equivalence to avoid ambiguity.
