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?
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.