Buenas, unas pregunta, la sustitución en este teorema se hace solo en 
o se hace en la formula con el para todo incluido? O sea, se hace primero la sustitucion y a eso despues lo cuantificamos en z o x o primero cuantificamos y despues sustituimos?
Hola.
No. La idea es sustiuir primero y cuantificar después.
Si queremos leer el teorema "en criollo", lo que nos dice es que:
Si en la fórmula 
, en el lugar de la variable 
ponemos 
y cuantificamos sobre , obtenemos una fórmula equivalente a que si en la misma fórmula ponemos la variable 
en el lugar de y usamos la misma cuantificación.
Parece entreverado, pero creo que no lo es tanto: En cambiamos y luego cuantificamos. No nos importa cómo se llama la variable que se pone en el lugar de , son fórmulas equivalentes.
Intenten demostrarlo y van a darse cuenta por qué funciona...
Espero haber aclarado (y no entreverado más :-) ) algo..
Saludos
FDO.
Hola.
Voy a escribir el teorema con parentesis extra a ver si queda más claro.
![(\forall x)(\alpha[x/y])\, eq\, (\forall z)(\alpha[z/y])](https://eva.fing.edu.uy/filter/tex/pix.php/65b76f9e6c44fa499eb7203b45fe1451.png "(\forall x)(\alpha[x/y])\, eq\, (\forall z)(\alpha[z/y])")
Capaz que así se entiende mejor.
La idea es que en 
se cambian las por y las por y luego se cuantifica.
Al momento de hacer esas sustituciones, no están hechas aún las cuantificaciones.
En criollo:
Puedo cambiar los nombres de las variables ligadas y obtengo fórmulas equivalentes.
Espero que haya quedado más claro.
Saludos
FDO.