Сама подмена

на выражение есть очень привычная замена переменной на её значение
Речь идёт о схеме аксиом, то есть, о способе записи бесконечного множества аксиом. Здесь для каждой высказывательной функции

определяется своя аксиома. Схема аксиом формулируется не в языке предметной теории (здесь — теории множеств), а в метаязыке, в котором определяется язык предметной теории (чаще всего это просто естественный язык). Поэтому к предметной теории эти замены отношения не имеют.
Да, конечно, но сам логический вывод имеет место быть и для палок
К сожалению, у нас нет формализованной теории палок. Когда Вы её создадите, тогда будете говорить о логическом выводе в теории палок и сравнивать его с логическим выводом в теории множеств.
Вообще в изложении того же Куратовского и Мостовского фигурируют два понятия - элемент и множество.
Тяжёлый случай. Я не понимаю, как можно было вычитать такое в тексте данной книги. Фраза "

является элементом множества

" является словесной записью формулы

, то есть, слово "элемент" — это ссылка на символ "

" в формуле. Теория, излагаемая в книге Куратовского и Мостовского — это ZFC минус аксиома регулярности и плюс аксиома реляционных типов. В ней нет никаких "элементов", кроме множеств.
в выражении указано обязательное условие - икс принадлежит игрек
Нет там никакого "обязательного условия". В этом месте доказательства происходит консервативное расширение языка теории множеств: вводится постоянная "

", и для этой постоянной формулируется аксиома

которая служит определением множества

(словами: произвольно взятое множество

является элементом множества

тогда и только тогда, когда

является элементом самого себя). Сокращённо это записывается как

(словами:

— множество всех таких множеств, каждое из которых является элементом самого себя). Делается это просто для удобства. В свою очередь, запись аксиомы также является сокращением, а полная запись может выглядеть, например, так:

В рассматриваемом выражении ясно указано - икс входит в игрек
Но точно так же икс входит и в игрек.
Это какое-то недоразумение. "

" и "

" — это просто символы. Они "входить" друг в друга не могут. В данном случае они используются как имена некоторых множеств (постоянная "

" является именем некоторого вполне определённого множества, а переменная

— именем произвольно взятого множества).
Вы явно перепутали два совершенно разных понятия: «буква "

" входит в формулу

» (это означает, что если мы посмотрим на запись формулы, например, "

", то в этой записи найдём букву "

") и «число

входит в число

» (никакое число ни в какое другое не входит; не надо придумывать какой-нибудь специальный смысл для этого "входит"; множества тоже не "входят" друг в друга).