Квантор Ⅎ на metamath.org

[Qlin]

http://us.metamath.org/mpeuni/df-nfc.html
Не могу понять суть определения символа $\underline{\Finv}$.
Квантор $\underline{\Finv}$ определяется по правилу:
$\underline{\Finv}x \ \ A \longleftrightarrow \forall y \Finv x \ \ y \in A$
Квантор $\Finv$ в свою очередь определяется по правилу:
$\Finv x \ \ \varphi \longleftrightarrow \forall x \ \ (\varphi \longrightarrow \forall x \ \ \varphi) $

В чём смысл ? Ведь если $y \in A$ является well formed формулой, то она и так не содержит свободной переменной $x$. Навешивание на неё квантора $\Finv$ ничего не изменит.

[kotenok gav]

Это означает, что $A$ не зависит от $x$. И по ссылке так и написано.

[Qlin]

kotenok gav, а можно увидеть какой-нибудь пример класса, который зависит от $x$ ? Скажем, класс всех множеств, определяемый, как $\{ x \mid \exists y \ \ x \in y \} $, зависит от $x$ ? А тот же класс всех множеств, определенный, как $\{ y \mid \exists x \ \ y \in x \}$, зависит от $x$ ?

-- 17.09.2021, 23:54 --

А класс всех множеств $\{ z \mid z \in x \lor z \notin x \}$ зависит от $x$ ?

[iifat]

Нет и нет на оба последних вопроса. $A(x)$ зависит от $x$, $\forall x A(x)$ — не. А вот подформула вашей первой формулы, например ($\{x|$) — зависит.

[Xaositect]

Например, $\mathcal{P} x$ зависит от $x$.