Buenas tardes profesor, muchas gracias por responder y por haberse tomado el tiempo de discutir el asunto con otro docente para elaborar su respuesta.
Lo que me pasó con el ejercicio por el que pregunté fue que empecé la demostración ("de arriba hacia abajo") desglosando la hipótesis que incluye cuantificadores universales, entonces como en la regla de eliminación de ese cuantificador se aplica la sustitución luego de eliminarlo, al seguir haciendo el ejercicio me quedé con esa idea. Entonces al ver que decía 
me surgió la duda, pero en realidad era que estaba leyendo mal la aplicación de la sustitución (en el existencial la sustitución se tiene antes de introducirlo), ahora ya claramente veo que la sustitución de x por y se hizo sobre todas las ocurrencias libres de y.
A pesar de que me di cuenta de eso mientras escribía la pregunta, al final decidí enviarla para ver a qué se debía eso que cité del libro, así que nuevamente le agradezco por haberse tomado el trabajo de habérmelo explicado.
Saludos,
Bruno Hernández.-