Two basic logic questions I'm pretty sure that these two logical moves are okay, but I just wanted to be sure.  If there are any subtleties (e.g. they are okay in first-order logic but not in more complex systems), please let me know.
1) Can you universally instantiate a negated proposition?  I.e. can you move from:
$ \left ( \forall x \right )\left ( x \rightarrow Y \right ) $
to
$ \neg b \rightarrow Y $?
2) Can you use rules of replacement within the scope of an operator?  I.e. can you move from:
$ \left ( \forall x \right )\left ( x \vee Y \right ) $
to
$ \left ( \forall x \right ) \neg \left (\neg x \& \neg Y \right ) $?
I think these two moves are okay but just want to be sure.  Thanks!
 A: In the first case, it would be better to instantiate a variable or a constant. You could define: $a =\lnot b$, in which case you could use universal instantiation $a$ as a witness, to get $a \rightarrow Y$, and then use rule of replacement by identity to get $\lnot b \rightarrow Y$.
Yes you can, in the second case; anything within the scope of the quantifier should be legitimate. However, it would probably be best to universally instantiate, using a witness, say $a$, to first get $a \lor Y$, and then $\lnot(\lnot a \land \lnot Y)$, assuming your formal system includes rules of replacement, based on logical identities, e.g., by DeMorgan's. That allows you to use the original universally quantified statement more directly (instantiating, for example $b \lor Y$, if you should choose to do so for another witness.
A: *

*I suppose You should only be allowed to instantiate with variables and constants. 

*Yes, you can. This is a shortcut to
$(\forall x)\phi(x)\vdash \phi(x)$ entails $\phi(x)$ by specialization, entails $\psi(x)$ by whatever rules you have in mind, entails $(\forall x)\psi(x)$ by generalization
