In "Elements of Set theory" by Enderton 54~55p
We can form something like the Cartesian product of infinitely many sets, provided that the sets are suitably indexed. More specifically, let $I$ be a set (which we will refer to as the index set) and let $H$ be a function whose domain includes $I$. Then for each $i$ in $I$ we have the set $H(i)$; we want the product of the $H(i)$'s for all $i \in I$. We define: $$X_{i\in I} H(i) = \{f\;|\; f \;\text{is a function with domain}\; I \;\text{and}\; (\forall i\in I)f(i)\in H(i)\}.$$
Axiom of Choice $\;$(second form) $\;$For any set $I$ and any function $H$ with domain $I$, if $H(i) \not =\emptyset$ for all $i$ in $I$, then $X_{i\in I} H(i) \not = \emptyset$.
The axiom has the form $\forall i\in I$, if $p(i)$ then $q(i) \iff \forall i$, if $i\in I$ then $(\text{if}\; p(i)\;\text{then}\; q(i))$. In particular, the statement is vacuously true when $I = \emptyset$. Is it necessary that we have this vacuously true part in the axiom?
There's no rule that every axiom in an axiomatization has to be independent of the other axioms. It's perfectly acceptable for an axiom to be provable from other axioms. (It's true that this would be redundant, so it would then be fine to remove the unnecessary axiom from the axiomatization, but there's no need to remove it.)
The same thing applies in the situation you mentioned. The axiom of choice in the form you stated is trivially true if $I = \emptyset.$ So it would be acceptable to replace the axiom
$$\text{"For any set }I\text{ and any function }H\text{ with domain }I\text{,}\\ \text{if }H(i) \not =\emptyset\text{ for all }i \in I\text{, then }\mathop{\vcenter{\huge\times}}_{i\in I} H(i) \not = \emptyset"$$
with
$$\text{"For any }\textbf{non-empty}\text{ set }I\text{ and any function }H\text{ with domain }I\text{,}\\ \text{ if }H(i) \not =\emptyset\text{ for all }i \in I\text{, then }\mathop{\vcenter{\huge\times}}_{i\in I} H(i) \not = \emptyset."$$
In fact, you could require $I$ to be infinite, since the axiom of choice for finite $I$ is provable from the axioms of ZF (without AC).
It wouldn't make any difference in terms of what you could prove.
However, there's a benefit in keeping the axioms as simple and as uniformly applicable as possible, so most people wouldn't want to restate the axiom of choice in this way.