Сама подмена 

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

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

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

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

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

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

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

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

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

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

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

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

 (словами: 

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

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

" и "

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

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

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

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

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

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

") и «число 

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

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