At PlanetMath there is the following theorem:
Theorem: If $H$ is a complete Heyting algebra, then $x\to y=\bigvee\{z\mid z\wedge x\le y\}$.
Proof: For any $a\in H$, we have $a\leq x\to y$ iff $a\wedge x\leq y$ iff $a\in\{z\mid z\wedge x\leq y\}$ iff $a\leq\bigvee\{z\mid z\wedge x\leq y\}$. ∎
The final step in this proof does not appear to be correct. I see no reason to believe that $a\leq\bigvee A$ implies $a\in A$, although the converse is certainly true. What's the right way to prove this theorem?
If $a\le\bigvee\{z\mid z\wedge x\le y\}$, then $a\wedge x\le \bigvee\{z\mid z\wedge x\le y\}\wedge x=\bigvee\{z\wedge x\mid z\wedge x\le y\}\le y$, where we are using the distribution of meet over infinite join proved in the other part of the theorem.
Alternatively, we can prove the theorem more simply as $$\bigvee\{z\mid z\wedge x\le y\}=\bigvee\{z\mid z\le x\to y\}=x\to y,$$ since $\bigvee\{z\mid z\le a\}\le a$ by $z\le a\Rightarrow z\le a$, and $$a\le a\Rightarrow a\in\{z\mid z\le a\}\Rightarrow a\le\bigvee\{z\mid z\le a\}.$$