don't understand this proof Let $d$ be a correspondence where $\emptyset \neq d(S) \subseteq S$ and two properties: A and B.
A) If $y, y' \in A \cap B$ and $y \in d(A)$, then $y \in d(B)$ whenever $y' \in d(B)$
B) If $Y \subseteq Z$, then $d(Z) \cap Y \subseteq d(Y)$
I'm having problems understanding this proof that shows that A implies B:
Let $y \in d(Z) \cap Y$. Since $d(Y) \neq \emptyset $, fix $y' \in d(Y) \subseteq Z$. Then, $y,y' \in Y \cap Z$ and by A) happens that $y \in d(Y)$.
This is a very short proof, but I don't get the logic behind it. It confuses me as it starts with property B (1), then uses A(2), and finally  use property B again (3).
(1) Let $y \in d(Z) \cap Y$. Since $d(Y) \neq \emptyset $, fix $y' \in d(Y) \subseteq Z$
(2)Then, $y,y' \in Y \cap Z$ 
(3) happens that $y \in d(Y)$.
I mean, if we are trying to proof that A implies B, as we are not using transposition shouldn't we start with A and then reach B?
EDIT
Thanks, the proof is much clearer this way.
For the development of the proof, I understand the importance of choosing $y, y'$ s.t. $y \in d(Z) \cap Y$ and $y' \in d(Y)$. 
It's obvious that we need to start with $y \in d(Z) \cap Y$ since we need to get to $y \in d(Y)$, but, for me, it is hard to come up with the idea of choosing a $y'$ s.t. $y' \in d(Y)$.
 A: The proof does start by assuming (A); the author simply takes it for granted that the reader will realize this. Here’s an expanded version of exactly the same argument.

Assume (A). We wish to show that if $Y\subseteq Z$, then $d(Z)\cap Y\subseteq d(Y)$, so assume that $Y\subseteq Z$. One way to show that $d(Z)\cap Y\subseteq d(Y)$ is to show that if $y\in d(Z)\cap Y$, then $y\in d(Y)$, so suppose that $y\in d(Z)\cap Y$. By hypothesis $d(Y)\ne\varnothing$, so there is some $y'\in d(Y)$. Since $d(Y)\subseteq Y\subseteq Z$ by hypothesis, $y'\in Y\cap Z$. Moreover, $y\in d(Z)\subseteq Z$, and $y\in Y$, so $y\in Y\cap Z$ as well. Thus, we have $y,y'\in Y\cap Z$, $y\in d(Z)$, and $y'\in d(Y)$, so (A) implies that $y\in d(Y)$. Since $y$ was an arbitrary member of $d(Z)\cap Y$, it follows that $d(Z)\cap Y\subseteq d(Y)$, as desired.

Does that make the flow of logic a bit clearer?
A: This is not a direct answer to your original question: Brian M. Scott did a great job clarifying the proof you quoted.
However, I'd like to show a proof in a different style, in answer to your later note that "for me, it is hard to come up with the idea of choosing a $\;y'\;$ s.t. $\;y' \in d(Y)\;$." So let's try to prevent rabbits being pulled out of hats.$
\newcommand{\calc}{\begin{align} \quad &}
\newcommand{\op}[1]{\\ #1 \quad & \quad \unicode{x201c}}
\newcommand{\hints}[1]{\mbox{#1} \\ \quad & \quad \phantom{\unicode{x201c}} }
\newcommand{\hint}[1]{\mbox{#1} \unicode{x201d} \\ \quad & }
\newcommand{\endcalc}{\end{align}}
\newcommand{\ref}[1]{\text{(#1)}}
\newcommand{\then}{\Rightarrow}
\newcommand{\when}{\Leftarrow}
\newcommand{\true}{\text{true}}
\newcommand{\false}{\text{false}}
$
In this style of proof (for background and details on notation see, e.g., Edsger W. Dijkstra's EWD1300) one tries to use shape of the formulas to guide the proof.  So we might as well start with writing our task a bit more formally: given
\begin{align}
& \tag{da} d(S) \not= \emptyset & \\
& \tag{db} d(S) \subseteq S & \\
& \tag{A} \langle \forall y,y' : y,y' \in A \cap B \;\land\; y \in d(A) \;\land\; y' \in d(B) : y \in d(B) \rangle & \\
& \tag{B1} Y \subseteq Z
\end{align}
for any sets $\;S, A, B\;$ and for some specific sets $\;Y, Z\;$, we are asked to prove
$$
\tag{B2} d(Z) \cap Y \subseteq d(Y)
$$
Our conclusion $\ref{B2}$ is cast in terms of sets, while the main hypothesis $\ref A$ is mostly given in terms of elements.  Therefore we have two options: we can either first transform $\ref A$ to sets, and then do the proof at the set level; or we can translate $\ref{B2}$ to elements and do the proof on the element level.  I've here chosen to do the latter, since I am more familiar with the laws of logic than the corresponding laws of set theory; but the choice seems fairly subjective.

So we start rewriting the conclusion $\ref{B2}$ in terms of elements, and see where that leads us:
$$\calc
    \tag{B2}
    d(Z) \cap Y \subseteq d(Y)
\op=\hint{expand definitions of $\;\subseteq\;$ and $\;\cap\;$}
    \langle \forall y : y \in d(Z) \;\land\; y \in Y : y \in d(Y) \rangle
\op=\hints{$\;Y = Z \cap Y\;$ by $\ref{B1}$; reorder}
       \hints{-- this makes the formula look more like}
       \hint{$\ref A$ (with $\;Z,Y\;$ substituted for $\;A,B\;$)}
    \langle \forall y : y \in Z \cap Y \;\land\; y \in d(Z) : y \in d(Y) \rangle
\op\when\hints{generalize, assuming there is some $\;y'\;$}
       \hints{for which $\;y' \in Z \cap Y\;$ and $\;y' \in d(Y)\;$}
       \hint{-- this brings us directly to $\ref A$}
    \langle \forall y,y' : y,y' \in Z \cap Y \;\land\; y \in d(Z) \;\land\; y' \in d(Y) : y \in d(Y) \rangle
\op=\hint{by $\ref A$ with $\;A,B := Z,Y\;$}
    \true
\endcalc$$
All that is left now is to prove that there is indeed a $\;y'\;$ for which $\;y' \in Z \cap Y \;\land\; y' \in d(Y)\;$:
$$\calc
    \langle \exists y' :: y' \in Z \cap Y \;\land\; y' \in d(Y) \rangle
\op=\hint{simplify using $\;Y = Z \cap Y\;$ by $\ref{B1}$}
    \langle \exists y' :: y' \in Y \;\land\; y' \in d(Y) \rangle
\op=\hint{RHS implies LHS, by $\ref{db}$}
    \langle \exists y' :: y' \in d(Y) \rangle
\op=\hint{by $\ref{da}$ and the definition of $\;\emptyset\;$}
    \true
\endcalc$$
And that completes the proof.
