I do not believe you need the additional axiom. The idea is to use the definability rule together with the fact we are using infinitary logic to get poor's man quantification over formuleas.

Let $φ=X=X$, and define $F_0=\{(c,m) \mid φ_m(c)\}$ where the $φ_i$ are the ones from the definability rule.

it is well defined because we are in $L_{ω_1,ω}$, if we want to be precise, let $ψ_i(x)=x\text{ is the 2-tuple $(y,k)$ and $k=i$ and $φ_i(y)$}$ then $F_0=\{x\mid \bigvee_{i\in\omega}ψ_i\}$.

The definability rule exactly states that for each class $C$ (and so each class $C$ such that $φ(C)$) there exists $m∈ω$ such that $F_0^{-1}(\{m\})=C$.

To get rid of duplicates entries simply note that "it wasn't previously defined" is definable in our language: define $F=\{(c,m)∈F_0\mid n<m\implies \text{there exists $d$ such that $φ_m(d)⇔¬φ_n(d)$}\}$.

Again, if we want to be precise, we can define the following sequence of formulaes, $η_i(m)=\left(m=i⇒\bigwedge_{j<i}∃d\left(φ_i(d)⇔¬φ_j(d)\right)\right)$ then $F=\{(c,m)\in F_0\mid \bigwedge_{i\in\omega}ν_i(m)\}$.

Clearly each class is still the preimage of some natural number, and if $m>n$ then $F^{-1}(\{m\})≠F^{-1}(\{n\})$.

Note that, assuming your theory is consistent, we get that $F$ is single definable using a finitary formula.

As stated in the comments, I misread the definition of the theory and assumed it is completely in infinitary logic, while in reality the ZFC+classes fragment is still in finitary logic, so the answer bellow is wrong

I do not believe you need the additional axiom. The idea is to use the definability rule together with the fact we are using infinitary logic to get poor's man quantification over formuleas.

Let $φ=X=X$, and define $F_0=\{(c,m) \mid φ_m(c)\}$ where the $φ_i$ are the ones from the definability rule.

it is well defined because we are in $L_{ω_1,ω}$, if we want to be precise, let $ψ_i(x)=x\text{ is the 2-tuple $(y,k)$ and $k=i$ and $φ_i(y)$}$ then $F_0=\{x\mid \bigvee_{i\in\omega}ψ_i\}$.

The definability rule exactly states that for each class $C$ (and so each class $C$ such that $φ(C)$) there exists $m∈ω$ such that $F_0^{-1}(\{m\})=C$.

To get rid of duplicates entries simply note that "it wasn't previously defined" is definable in our language: define $F=\{(c,m)∈F_0\mid n<m\implies \text{there exists $d$ such that $φ_m(d)⇔¬φ_n(d)$}\}$.

Again, if we want to be precise, we can define the following sequence of formulaes, $η_i(m)=\left(m=i⇒\bigwedge_{j<i}∃d\left(φ_i(d)⇔¬φ_j(d)\right)\right)$ then $F=\{(c,m)\in F_0\mid \bigwedge_{i\in\omega}ν_i(m)\}$.

Clearly each class is still the preimage of some natural number, and if $m>n$ then $F^{-1}(\{m\})≠F^{-1}(\{n\})$.

Note that, assuming your theory is consistent, we get that $F$ is single definable using a finitary formula.