Is "$(\forall x \,\,x\in X)\implies x\in Y$ holds for any sets $X$ and $Y$" really a proposition? I am reading "Set Theory and General Topology" by Takeshi SAITO (in Japanese).
The author wrote as follows:

Since $\forall x \,\,x\in X$ doesn't hold for any set $X$, $(\forall x \,\,x\in X)\implies x\in Y$ holds for any sets $X$ and $Y$.

I think $x\in Y$ is not a proposition since we don't know what $x$ is.
So I think "$(\forall x \,\,x\in X)\implies x\in Y$ holds for any sets $X$ and $Y$" is not a proposition.
Am I wrong?
 A: Assuming that you are working in $\mathsf {ZFC}$ (or similar) where there is no "universal set", we have that: $\lnot \exists X \forall x (x \in X)$ which is equivalent to: $\forall X \lnot \forall x (x \in X)$.
Thus, using the tautology: $\lnot P \to (P \to Q)$, we derive:

$\forall x (x \in X) \to (x \in Y)$,

and thus: $\forall X \forall Y [\forall x (x \in X) \to (x \in Y)]$.
The formula $\forall x (x \in X) \to (x \in Y)$ is not a sentence but an open formula, i.e. a formula with a free occurrence of a variable, but it is syntactically correct one.
Usually, an open formula is read as universally quantified; thus, it is equivalent to: $\forall x (x \in X) \to \forall x(x \in Y)$.
A: It's a fair question.  If I recall my Logic class (taught by Peter Andrews), that instance of $x$ is unbound, which is fair.  In fact, $Y$ is also an unbound variable, and we understand that it probably has some special meaning outside the context of this sentence.  It is important to keep in mind that it is not the same as the $x$ that is inside the parentheses, which is bound by the universal instantiation.
Stylistically, I think that it is inelegant at best to put $x$ to dual use like that, but I believe it is a well-formed statement.
