# Metamath Proof Explorer

## Definition df-nfc

Description: Define the not-free predicate for classes. This is read " x is not free in A ". Not-free means that the value of x cannot affect the value of A , e.g., any occurrence of x in A is effectively bound by a "for all" or something that expands to one (such as "there exists"). It is defined in terms of the not-free predicate df-nf for wffs; see that definition for more information. (Contributed by Mario Carneiro, 11-Aug-2016)

Ref Expression
Assertion df-nfc ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}↔\forall {y}\phantom{\rule{.4em}{0ex}}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {A}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 vx ${setvar}{x}$
1 cA ${class}{A}$
2 0 1 wnfc ${wff}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
3 vy ${setvar}{y}$
4 3 cv ${setvar}{y}$
5 4 1 wcel ${wff}{y}\in {A}$
6 5 0 wnf ${wff}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {A}$
7 6 3 wal ${wff}\forall {y}\phantom{\rule{.4em}{0ex}}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {A}$
8 2 7 wb ${wff}\left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}↔\forall {y}\phantom{\rule{.4em}{0ex}}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {A}\right)$