$P \to Q \equiv \neg P \vee Q$ Most of the textbook that I had went through proves the given equivalence using truth table.
But is there any way of proving $P \to Q \equiv \neg P \vee Q$  without truth table?
 A: $(1)\quad$ Prove: $(P\rightarrow Q)\rightarrow(\neg P\vee Q)$ and 
$(\neg P\vee Q)\rightarrow (P\rightarrow Q)$
$(2)\quad$ Assume $P\rightarrow Q$ and assume $P$, then $Q$
$(3)\quad$ and therefor $\neg P\vee Q$
$(4)\quad$ if $\neg P$ then also $\neg P\vee Q$. 
$(5)\quad$ Reversed, assume $\neg P\vee Q$. If $Q$ then $P\rightarrow Q$. 
$(6)\quad$ And if $\,\neg P$ then also $P\rightarrow Q$. 
$\therefore$ $(P\rightarrow Q)\equiv(\neg P\vee Q)$

$(1)\quad ((f\rightarrow g) \wedge (g\rightarrow f))\equiv (f\equiv g)$ 
$(2)\quad ((f\rightarrow g)\wedge f)\rightarrow g$
$(3)\quad f\rightarrow (f\vee g)$
$(4)\quad f\rightarrow (f\vee g)$
$(5)\quad g\rightarrow (f\rightarrow g)$
$(6)\quad \neg f\rightarrow (f\rightarrow g)$
A: In many formal systems you don't have both $\to$ and $\lor$, rather one of them is defined. For example, in Hilbert-style systems it is popular to have $\to$ as a primitive and define $\lor$ essentially using the equivalence you note, while in the sequent calculus we usually have $\lor$ and define $\to$ using your equivalence. In such systems there is no need to prove this equivalence, since it is true by definition.
Other systems, such as natural deduction, do contain both $\to$ and $\lor$ as primitive notions. It is then an easy exercise to prove your equivalence given the axioms of the system. If you're curious, you can look up natural deduction and give it a shot yourself.
