Lets work with Harvey's Friedman theory ${\sf K}(W)$, formulated in the language of set theory with a primitive constant symbol $W$ added, i.e. in ${\sf FOL}(\in,W)$

**Axioms:**

**Extensionality:** $$\forall Z \, (Z \in X \iff Z \in Y) \implies \\\forall Z \, (X \in Z \iff Y \in Z)$$

**Subworld Separation:** $$\forall A \in W \, \exists X \in W \, \forall Y \, (Y \in X \iff Y \in A \land \phi)$$; where formula $\phi$ doesn't use the symbol "$X$".

**Reducibility:** if $\phi$ is a formula in ${\sf FOL} (\in)$, with all parameters among "$X,\vec{P}$ " then: $$\forall \vec{P} \in W [ (\exists X: \phi) \implies \exists X \in W: \phi]$$

/

Which is equiconsistent with ZFC.

Is it consistent to add the following principle:

**Generalization:** if $\phi$ is a formula in ${\sf FOL} (\in)$, with all parameters among symbols "$X,\vec{P}$ "; then: $$ \forall \vec{P} \in W [(\forall \operatorname {infinite} X \in W: \phi) \implies \phi(W)]$$