A choice-free proof of Mal'cev's theorem on quasivarieties

In 1966, Mal’cev proved that a class $\mathcal{K}$ of first-order structures with a specified signature is a quasivariety if and only if $\mathcal{K}$ contains a unit and is closed under isomorphisms, substructures, and reduced products. In this article, we present a proof of this theorem in $\mathsf{Z}\mathsf{F}$ (the Zermelo–Fraenkel set theory without the axiom of choice).