Prove if $B$ has a smallest element, then this element is unique. Working on the book: Daniel J. Velleman. "HOW TO PROVE IT: A Structured Approach, Second Edition" (p. 206)

Theorem 4.4.6. Suppose $R$ is a partial order on a set $A$, and $B \subseteq A$.
If $B$ has a smallest element, then this smallest element is unique. Thus, we
  can speak of the smallest element of $B$ rather than a smallest element.

I symbolized "$B$ has a smallest element", as: $$\exists y\forall x(x \in B \to (y,x) \in R)$$
"$B$ smallest element is unique", as: $$\exists y(\forall x(x \in B \to (y,x) \in R) \land \forall z(\forall x(x \in B \to (z,x) \in R) \to y = z))$$
My proof skeleton using Fitch-style natural deduction:
$
\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}
\def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\}
\def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\}
\def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\}
\def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\}
\def\R#1{\qquad\mathbf{R} \: #1 \\}
\def\ci#1{\qquad\mathbf{\land I} \: #1 \\}
\def\ce#1{\qquad\mathbf{\land E} \: #1 \\}
\def\oi#1{\qquad\mathbf{\lor I} \: #1 \\}
\def\oe#1{\qquad\mathbf{\lor E} \: #1 \\}
\def\ii#1{\qquad\mathbf{\to I} \: #1 \\}
\def\ie#1{\qquad\mathbf{\to E} \: #1 \\}
\def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\}
\def\bi#1{\qquad\mathbf{\leftrightarrow I} \: #1 \\}
\def\qi#1{\qquad\mathbf{=I}\\}
\def\qe#1{\qquad\mathbf{=E} \: #1 \\}
\def\ne#1{\qquad\mathbf{\neg E} \: #1 \\}
\def\ni#1{\qquad\mathbf{\neg I} \: #1 \\}
\def\IP#1{\qquad\mathbf{IP} \: #1 \\}
\def\x#1{\qquad\mathbf{X} \: #1 \\}
\def\DNE#1{\qquad\mathbf{DNE} \: #1 \\}
$
$
\fitch{1.\, \exists y\forall x(x \in B \to (y,x) \in R)}{
 \fitch{2.\, \forall x(x \in B \to (b',x) \in R)}{
 \fitch{3.\, \forall x(x \in B \to (b,x) \in R)}{
   4.\,b \in B \to (b',b) \in R \Ae{2}
   5.\,b \in B \to (b,b') \in R \Ae{3}
   \vdots\\
}\\
b=b'\\
}\\
\forall x(x \in B \to (z,x) \in R) \to y = z)
}
$
As $R$ is a partial order, I would need to use antisymmetry property. But I do not know how to use it in lines 4,5 to infer that $(b',b) \in R \land (b,b') \in R$.
How can I fill the dots ? Am I missing some premise or step?
 A: Preliminary: I use the notation $xRy$ for $(x,y) \in R$.
Remark: The correct formalization of "$B$ has a smallest element" is 
$$\exists y(y \in B \land \forall x(x \in B \to yRx))$$
It is important that smallest element of $B$ is in $B$, otherwise you lose uniqueness. Indeed, let $A = \{a_1, a_2, b\}$ and $ B = \{b\}$ with $a_1 < b$ and $a_2 < b$ and $a_1 \neq a_2$: both $a_1$ and $a_2$ (which are distinct) satisfy $\exists y \forall x (x \in B \to yRx)$ (I assume the domain of quantifications is $A$).
Solution: First, consider the following proof $\pi$ in Fitch-style natural deduction of the fact that if $R$ is a antisymmetric relation (on the domain $A$, premise $0$) and if $y$ is a smallest element of $B$ (premise $1$), then any other smallest element of $B$ is equal to $y$.
$
\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}
\def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\}
\def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\}
\def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\}
\def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\}
\def\R#1{\qquad\mathbf{R} \: #1 \\}
\def\ci#1{\qquad\mathbf{\land I} \: #1 \\}
\def\ce#1{\qquad\mathbf{\land E} \: #1 \\}
\def\oi#1{\qquad\mathbf{\lor I} \: #1 \\}
\def\oe#1{\qquad\mathbf{\lor E} \: #1 \\}
\def\ii#1{\qquad\mathbf{\to I} \: #1 \\}
\def\ie#1{\qquad\mathbf{\to E} \: #1 \\}
\def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\}
\def\bi#1{\qquad\mathbf{\leftrightarrow I} \: #1 \\}
\def\qi#1{\qquad\mathbf{=I}\\}
\def\qe#1{\qquad\mathbf{=E} \: #1 \\}
\def\ne#1{\qquad\mathbf{\neg E} \: #1 \\}
\def\ni#1{\qquad\mathbf{\neg I} \: #1 \\}
\def\IP#1{\qquad\mathbf{IP} \: #1 \\}
\def\x#1{\qquad\mathbf{X} \: #1 \\}
\def\DNE#1{\qquad\mathbf{DNE} \: #1 \\}
$
$
\fitch{0. \, \forall y \forall z (yRz \land zRy \to y = z)
 \\
  1.\, y \in B \land \forall x (x \in B \to yRx)}
{
 \fitch{2.\, z \in B \land \forall x (x \in B \to zRx)}
    {3. \, \forall x (x \in B \to zRx) \ce{2}
     4. \, y \in B \to z R y \Ae{3}
     5. \, y \in B \ce{1}
     6. \, zRy \ie{4,5}
     7. \, \forall x (x \in B \to yRx) \ce{1}
     8. \, z \in B \to yRz \Ae{7}
     9. \, z \in B \ce{2}
    10. \, yRz \ie{8,9}
    11. \, yRz \land zRy \ci{10, 6}
    12. \, yRz \land zRy \to y = z \Ae{0}
    13. \, y = z \ie{12,11}
}\\
 14. \, (z \in B \land \forall x (x \in B \to zRx)) \to y = z \ii{2{-}13}
 15. \, \forall z \big((z \in B \land \forall x (x \in B \to zRx)) \to y = z \big) \Ai{14}
}
$
Given the proof $\pi$ above, it is immediate to write a proof in Fitch-style natural deduction of 
\begin{equation}\tag{*}
\exists y \big( y \!\in\! B \land \forall x (x \!\in\! B \to yRx) \land \forall z ((z \!\in\! B \land \forall x (x \!\in\! B \to zRx)) \to y = z) \big)
\end{equation}
under the assumptions that $R$ is antisymmetric (premise $0$ below) and that $B$ has a smallest element (premise $1$ below):
$
\fitch{0. \, \forall y \forall z (yRz \land zRy \to y = z)
 \\
  1.\, \exists y (y \in B \land \forall x (x \in B \to yRx))}
{
 \fitch{2.\, y \in B \land \forall x (x \in B \to yRx)}{
    \vdots \ \pi
    \\
    16. \, \forall z \big((z \in B \land \forall x (x \in B \to zRx)) \to y = z \big) \\
    17. \, (y \!\in\! B \land \forall x (x \!\in\! B \to yRx)) \land \forall z \big((z \!\in\! B \land \forall x (x \!\in\! B \to zRx)) \to y = z \big) \ci{2, 16}
    18. \, \exists y \big( (y \!\in\! B \land \forall x (x \!\in\! B \to yRx)) \land \forall z \big((z \!\in\! B \land \forall x (x \!\in\! B \to zRx)) \to y = z \big) \big) \Ei{17}
    }\\
  19. \, \exists y \big( (y \!\in\! B \land \forall x (x \!\in\! B \to yRx)) \land \forall z \big((z \!\in\! B \land \forall x (x \!\in\! B \to zRx)) \to y = z \big) \big) \Ee{1, 2{-}18}
}
$
Note that formula $(*)$ above formalizes the sentence "$B$ has a unique smallest element".
Final remark: Actually the derivation above shows that only antisymmetry of $R$ is required to prove the uniqueness of the smallest element. Transitivity and reflexivity of $R$ play no role.
