Disjunctive introduction rule ( i.e OR intro ) for predicate logic :freely introducing OR inside a quantified sentence?

Question

While I was trying to answer this question : find a counter example to the statement $\forall_{x \in C}(\exists_{y \in C}(y \in A) \Rightarrow \neg (x \in B)) .$

I asked myself whether this move is legal in predicate logic :

(1) There is some x that does not belong to C

therefore

(2) There is some x such that ( x does not belong to C OR whatever )

Is it legal to use " OR intro" inside a quantified formula? Does a quantified formula remain true in case I really add " whatever" I want as disjunct?

Answer 1

Yes because for (1) to be true means that (1) holds in all models. But (2) is weaker than (1) in each model separately, so this move is indeed legal (as long as whatever is a valid formula in the language, of course).