А если говорить о некоторых связях, можно связать

и с импликацией. Однако чтобы понять, чем эти связи являются и чем нет, сначала нужно разобраться с собственно исчислением предикатов, чтобы была ну хоть какая-то база.
Почему я и использовал именно Куратовского, так это именно потому, что он подробно и в аксиоматическом виде, то есть не пропуская этапов вывода, даёт теорию множеств. Поэтому он сначала говорит про алгебру высказываний, потом про высказывательные функции и кванторы, то есть даёт хоть и краткое, но изложение исчисления высказываний и предикатов. Значит "хоть какая-то" база им точно даётся.
Там ещё пишется, что

используется для случая, когда высказывательная функция

определена всюду.
Да. Но я встретил возражения двух более опытных участников с однозначным отрицанием правильности моего заявления про "для всех

", поэтому я и взял другую часть определения, которая так же приводит к некорректному переводу и доказательству.
Собственно такой вид квантора «первичен», такие используются в частности в теориях, ничего не говорящих о множествах, и даже для формализации теории множеств такой вид кванторов, как warlock66613 уже сказал, необходим, ну и сами авторы книги в этом от строгости не отходят, см. гл. II §2.
Более того, там в сноске на стр.54 даже указывается, что "вместо символов

используются и другие, например

".
Нет, мы могли бы удовлетвориться ограниченными кванторами, если бы у нас в частности было бы множество всех множеств.
Так в обоих случаях получается некорректность. Если "для всех", то теряется ограничение из нестрогого определения, а если "для всех принадлежащих", то не доказывается принадлежность и вводится произвольное множество

.
Можно считать, что смысл кванторов и связок задаётся только интерпретацией, а интерпретация языка первого порядка в некоторых книгах может откладываться, пока не рассмотрен будет вывод. (Это выглядит странно, но вроде бывают причины.)
До туда я пока не дошёл, поэтому не могу что-то уверенно говорить.
В целом же, рассуждая в терминах Куратовского, который все свои термины хорошо поясняет, у меня получилось то, что получилось. А дополнительно понять ситуацию с использованием исчисления предикатов у других авторов я пока не успел. Книга Френкеля у меня есть, так что постепенно и мнение автора ZF узнаю.