I use Lukasiewicz/Polish notation. Given intuitionistic logic with the optional axioms for equivalence and negation given in the Wikipedia, can
ECpqANpq or in other notation
[(p$\rightarrow$q)=($\lnot$p$\lor$q)] get proved in intuitionistic logic?
NO; in intuitionistic logic the "basic" connectives are independent.
See Jan von Plato, Elements of Logical Reasoning (2013), page 59 :
Independence of the connectives. We have seen that there are connections between the connectives, such as the derivable implications $A \land B \rightarrow ¬(¬A \lor ¬B), A \lor B \rightarrow ¬(¬A \land ¬B)$, and $(A \rightarrow B) \rightarrow ¬(A \land ¬B)$. It can be shown that none of the converse implications is derivable in intuitionistic logic. Further similar results show the following:
Independence of the connectives in intuitionistic logic. None of the connectives can be expressed equivalently by the remaining ones.
See also page 75 for an example regarding : $\nvdash ¬(¬ A \land ¬ B ) \rightarrow A \lor B$.
Regarding specifically the question about $(p → q) \leftrightarrow (¬p \lor q)$ we have :
$\vdash (¬p \lor q) \rightarrow (p → q)$
$\nvdash (p → q) \rightarrow (¬p \lor q)$.
Assuming $(p → q) \rightarrow (¬p \lor q)$, by substitution we get : $(p → p) \rightarrow (¬p \lor p)$.
But $\vdash p \rightarrow p$; thus by modus ponens we were able to prove the intitionistically invalid :
$(¬p \lor p)$.
For $\vdash (¬p \lor q) \rightarrow (p → q)$ :
1) $\lnot p \lor q$ --- assumed [a]
2) $\lnot p$ --- assumed [b] (it is the abbreviation for : $p \rightarrow \bot$)
3) $p$ --- assumed [c]
4) $\bot$ --- from 2) and 3) by modus ponens ($\rightarrow$-E)
5) $q$ --- from 4) by $\bot$-E
6) $p \rightarrow q$ --- from 3) and 5) by $\rightarrow$-I, discharging [c]
7) $q$ --- assumed [d]
8) $p \rightarrow q$ --- from 7) by $\rightarrow$-I
9) $p \rightarrow q$ --- from 8), 7), 6), 2) and 1), by $\lor$-E, discharging [b] and [d]
10) $(¬p \lor q) \rightarrow (p → q)$ --- from 9) and 1), by $\rightarrow$-I.