By equivalent I mean the biconditional, as in
$$\lnot (p \implies q) \iff p \land \lnot q$$
Given the definition of implication, I understand why this is true, but I need a bit of help showing this with a formal proof using rules like $\lor-\text{Elim}$ and $\bot-\text{Intro}$.
Best Answer
Here is the pure natural deduction proof (Fitch-Style).
If $p \land \neg q$:
$p$;
$\neg q$.
If $p \to q$:
...
$\bot$.
$\neg( p \to q )$.
If $\neg( p \to q )$:
If $\neg p$:
If $p$:
$\bot$.
$q$.
$p \to q$.
$\bot$.
$\neg \neg p$.
$p$.
If $q$:
...
$p \to q$.
$\bot$.
$\neg q$.
$p \land \neg q$.
$p \land \neg q \leftrightarrow \neg( p \to q )$.
I'll leave you to fill in the blanks, which should be easy. See this post for a brief description of the general method to discovering such a proof. Sometimes it can be convenient to use LEM (law of excluded middle) to split cases in a clever manner to shorten the proof, but that way requires some experience.
As for the interesting side question of whether or not one can prove the equivalence in intuitionistic logic, which has the same inference rules except without DNE (double negation elimination), and hence LEM does not hold, the answer is that indeed it cannot be done. Note that the above proof only uses DNE once. Feel free to ignore the rest of this post if you are not interested in intuitionistic logic.
In intuitionistic logic, "$\neg p$" is simply a short-form for "$p \to \bot$". To prove that some sentence is not provable in intuitionistic logic, it suffices to construct a Kripke frame that does not satisfy it (see this post). Consider the Kripke frame $0 \to 1$ where $p$ is known only at $1$ and $q$ is not known at both $0,1$. Then $\neg( p \to q )$, which denotes $( p \to q ) \to \bot$, is known everywhere, but $p \land \neg q$ is not known at $0$.
Alternatively, note that if it were provable in intuitionistic logic, it would hold when $q = \bot$, but that gives $\neg( p \to \bot ) \to p \land ( \neg \bot )$, which is equivalent (by definition) to $\neg \neg p \to p$, which is not valid in intuitionistic logic.