The second order rule of identity that depicts Leibenz definition of identity is
$\forall P (P(x) \leftrightarrow P(y)) \leftrightarrow x=y$,
has two directions: the first being identity of indiscernibles and the second called indiscernibility of identicals.
Now the first order identity theory with the reflexive axiom and the substitution axiom only captures the second direction.
Now if to first order identity theory we add the following $\omega$-rule to assure the first direction, would that add any strength to identity theory?
Identity of indscernibles $\omega$-inference rule: Let $\phi_1(X),\phi_2(X),...$ be all formulas in first order logic with the symbol $=$ added to it, in which the symbol $X$ occur free, and only free, and in which the symbol $Y$ doesn't occur. Let $\phi_i(Y|X)$ be the formula obtained by merely replacing some of the occurrences of symbol $X$ in $\phi_i(X)$ by symbol $Y$; Let $\psi(X), \varphi(Y)$ be any formulas in that language in which symbols $X$ and $Y$ occur free and only free respectively; let $\vec{p}$ represent the conjoined string of parameters in formulas $\psi, \varphi, \phi_i$; then:
From: $\big{[}for \ i=1,2,3,..., \\ \forall \vec{p} \ \forall X,Y (\psi(X) \land \varphi(Y) \to [\phi_i(X) \leftrightarrow \phi_i(Y|X)]) \big{]} $
_________________________________we infer
$ \forall \vec{p} \ \forall X,Y(\psi(X) \land \varphi(Y) \to X=Y)$
Now when we extend this theory, then the formulas containing the added primitives are among formulas in the above rule, much as they'll be with the substitution scheme.
So for example if we formalize $ZFC$ as an extension of this identity theory, would that have any impact on $ZFC$?