Смысл схемы преобразования (схемы аксиом подстановки) в том, что если у вас есть некоторая формула со свободными переменными
и
, причем одному
всегда соответствует только один
(свойство функциональности=однозначности), то образом множества будет множество (т.е. если
пробегает множество, то соответствующие
пробегают тоже некоторое множество).
В ней не говорится, что такая формула не может содержать еще какие-то параметры (точно так же, как схема индукции в арифметике).
Далее просто пишем такую формулу, которая реализует функцию
и
для любого непустого
и любых параметров
.
Теперь берем множество
, его образом будет
, которое есть некоторое множество по данной схеме аксиом.
Таким образом, в схеме аксиом две переменных
отвечают за реализацию функциональной зависимости, а переменные
и
- это параметры (свободные переменные).
Просто обычно в матлогике принято не указывать свободные переменные, если они никак не участвуют в формулировках. Подразумевается, что они могут быть добавлены в неограниченном количестве и закрыты кванторами всеобщности. И только если требуется уточнить наличие/отсутствие параметров (как, например, для схемы индукции без параметров), это оговаривается явным образом.