Etale morphisms are the formally etale morphisms locally of finite presentation

Forward direction, formal smoothness. Assume $f$ 'etale. Then $f$ is locally of finite presentation and smooth at every point by [F1], hence smooth [F6]; [F5] (AC) then shows that $f$ is formally smooth.

Forward direction, vanishing differentials. Assume $f$ 'etale. At every point $x$ the morphism $f$ is locally of finite presentation, flat and unramified, the last by [F2] (AC) in the forward direction; by [F3] this means ${\mathrm{\Omega }}_{X\mathrm{/}S,x}=0$. As $x$ ranges over $X$ the sheaf of relative differentials vanishes: ${\mathrm{\Omega }}_{X\mathrm{/}S}=0$, and on every affine chart $\mathrm{Spec}B$ over $\mathrm{Spec}A$ the module ${\mathrm{\Omega }}_{B\mathrm{/}A}$ is zero by [F7].

Reverse direction. Assume now that $f$ is locally of finite presentation and formally 'etale (AC). By [F4] $f$ is formally smooth and formally unramified; [F5] applied to the formally smooth morphism turns local finite presentation into smoothness, so $f$ is smooth, and consequently locally of finite presentation and flat at every point by [F6]. By [F3] the formal unramifiedness gives ${\mathrm{\Omega }}_{X\mathrm{/}S}=0$, hence $f$ is unramified at every point (it is locally of finite presentation, in particular locally of finite type); [F2] then gives that $f$ is 'etale at every point.

Forward direction, uniqueness of lifts. Let $i\text{\hspace{0.17em}⁣}:T_0\hookrightarrow T$ be a square-zero thickening, let $u,v\text{\hspace{0.17em}⁣}:T\to X$ be $S$-morphisms with $u{\mathrm{\mid }}_{T_0}=v{\mathrm{\mid }}_{T_0}$; we show $u=v$. Agreement is local on $T$ [F8], so fix $t\in T$ and put $y:=u(t)=v(t)$ (equality holds because a square-zero thickening has the same underlying space as $T$: the underlying map of a closed immersion is injective with image the closed set where the stalk of $\mathcal{I}$ is not the whole local ring, and a square-zero ideal has no stalk equal to the whole local ring, for that would force the local ring $0$). Choose affine opens $\mathrm{Spec}A=V\subseteq S$ around $f(y)$ and $\mathrm{Spec}B=U\subseteq X$ around $y$ with $f(U)\subseteq V$; then $W:=u^{-1}(U)\cap v^{-1}(U)$ is an open neighbourhood of $t$ and we may replace $T$ by an affine open $\mathrm{Spec}C\subseteq W$ containing $t$, so that $u,v$ correspond to $A$-algebra maps $\phi ,\psi \text{\hspace{0.17em}⁣}:B\to C$ agreeing modulo the square-zero ideal $I\subseteq C$ of $T_0\cap T$. Define $D:=\phi -\psi \text{\hspace{0.17em}⁣}:B\to I$. For $b,b^{\mathrm{\prime }}\in B$ one computes $D(b{b}^{\mathrm{\prime }})=\phi (b)\phi (b^{\mathrm{\prime }})-\psi (b)\psi (b^{\mathrm{\prime }})=\phi (b)D(b^{\mathrm{\prime }})+D(b)\psi (b^{\mathrm{\prime }})$, and since $\phi (b)-\psi (b)\in I$ and $I^2=0$ the elements $\phi (b)$ and $\psi (b)$ act in the same way on $I$, so $D$ is an $A$-derivation of $B$ into the $C$-module $I$. By [F7] and the vanishing ${\mathrm{\Omega }}_{B\mathrm{/}A}=0$ of step 1.2, $D=0$, so $\phi =\psi$ and $u=v$ on $\mathrm{Spec}C$; as $t$ was arbitrary, $u=v$ on $T$.

Forward direction, conclusion. By steps 1.1 and 2.1 the 'etale morphism $f$ is formally smooth (local existence of lifts) and formally unramified (uniqueness of lifts agreeing on a square-zero thickening), hence formally 'etale by [F4]; it is locally of finite presentation by [F1]. This proves the 'only if' direction.

Summary. The Axiom of Choice [F9] is assumed in the Statement and is used exactly through [F5] in steps 1.1 and 1.3 and through [F2] in steps 1.2 and 1.3; steps 2.1 and 3.1 use only the universal property of differentials and the definition of formal 'etaleness, and add no choice. [F2, F5, F9, step 1.1, step 1.2, step 1.3] $\mathrm{\square }$