Is My Proof Correct, & Alternatives: "A and B are logical equivalents iff A <-> B is a tautology" ** N.B. Boolean operators are represented by their computer equivalents: (a) ∧ == & (b) ∨ == | (c) ¬ == ~
Proposition: A is logically equivalent to B iff A <-> B is a tautology"
Proof:
1. (=>) Suppose A is logically equivalent to B.
            A <-> B = (A -> B) & (B -> A)
            = (~A | B) & (~B | A)
            = (~A | A) & (~B | B)        (logical eqivalence)
            = T & T                      [(x | ~x) = T]
            = T
    Therefore, by definition of "tautology" A <-> B is a tautology.

 2. (<=) Suppose A <-> B is a tautology.
            Then, by definition of "tautology" (A -> B) & (B -> A) = T
            => (A -> B) = T, and (B -> A) = T     (1)
            Now, (A -> B) = T <=> A  |  B
                                  -------
                                  T  |  T
                                  F  |  F
                                  F  |  T
            But, row 3 of the above truth table is impossible, as from (1) (B -> A) = T
            Therefore,  A  |  B
                        -------
                        T  |  T
                        F  |  F
    Therefore, by definition of "logical equivalence" A is logically equivalent to B    ∎

Is my proof correct, and can someone think of a more elegant way of proving this proposition (esp. the converse)?
 A: Your proof, though essentially correct, is a little bit of a strange mix of syntactical and semantical methods.
I also note that in the first half, you use the equivalence between A and B to rewrite the A as a B  and vice versa.  Again, this is correct, but it would require some meta-logical principle (the Principle of Substitution of Logical Equivalents, to be exact).
I think this proof can really be done a lot cleaner if you do it purely meta-logically. And, I would certainly recommend doing it that way, since for more complicated proofs you really want to do it that way, so this will be good practice.
So, what do I mean by this? ell, just use the definitions! That is:
$\phi$ is a tautology iff for every truth-value assignment $v$, we have that $v(\phi)=True$
$\phi$ and $\psi$ are logically equivaenet iff for every truth-valuation: $v(\phi) = v(\psi)$
And finally, by definition of the semantics of the $\leftrightarrow$, we have: $v(\phi \leftrightarrow \psi)=T$ iff $v(\phi)=v(\psi)$
OK, with those definitions, the proof is as follows:
$A$ is logically equivalent to $B$ iff (definition logical equivalence)
for every possible truth-value $v$ we have that $v(A)=v(B)$ iff (semantics $\leftrightarrow$)
for every possible truth-value $v$ we have that $v(A \leftrightarrow B)=T$ iff (definition tautology)
$A \leftrightarrow B$ is a tautology
And, since we used iff's every step of the way, that's it!!
