Is it consistent to add a generalization axiom on top of Ext.+Subworld Separation+Reduciblity?

Question

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)]$$

Answer 1

Generalization holds in K(W). Suppose it did not, that ¬𝜙(W) holds and ∀infinite𝑋∈𝑊:𝜙.

Then ∃X((infiniteX)∧¬𝜙), since this is true when X is W. By Reducibility

∃X∈W((infiniteX)∧¬𝜙). But this contradicts the fact that ∀infinite𝑋∈𝑊:𝜙.