Proof
(related to Lemma: Implication as a Disjunction)
Context
 Let $x,y$ be two propositions.
 We want to show that $(x\Rightarrow y)\Longleftrightarrow (\neg x \vee y).$
Hypothesis
 We are given the implication $x\Rightarrow y$.
Implications
\(\models(x)\) 
\(\models(y)\) 
\(\models(x \Rightarrow y)\) 
\(1\) 
\(1\) 
\(1\) 
\(0\) 
\(1\) 
\(1\) 
\(1\) 
\(0\) 
\(0\) 
\(0\) 
\(0\) 
\(1\) 
 Based on the truth tables of the negation and disjunction, the truth table of $(\neg x\vee y)$ is given by
\(\models(x)\) \(\models(y)\) \(\models(\neg x) \) \(\models(\neg x \vee y)\)
\(1\) \(1\) \(0\) \(1\)
\(0\) \(1\) \(1\) \(1\)
\(1\) \(0\) \(0\) \(0\)
\(0\) \(0\) \(1\) \(1\)
Conclusion
 Since the outcomes (columns to the right) of both truth tables are equal, we have shown the equivalence $(x\Rightarrow y)\Longleftrightarrow (\neg x \vee y).$
∎
Thank you to the contributors under CC BYSA 4.0!
 Github:

References
Bibliography
 Mendelson Elliott: "Theory and Problems of Boolean Algebra and Switching Circuits", McGrawHill Book Company, 1982