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 _ x A y x y A

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx setvar x
1 cA class A
2 0 1 wnfc wff _ x A
3 vy setvar y
4 3 cv setvar y
5 4 1 wcel wff y A
6 5 0 wnf wff x y A
7 6 3 wal wff y x y A
8 2 7 wb wff _ x A y x y A