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{\_}{Ⅎ}xA\leftrightarrow \forall yℲxy\in A$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		cA	$$classA$$
2	0 1	wnfc	$$wff\underset{\_}{Ⅎ}xA$$
3		vy	$$setvary$$
4	3	cv	$$setvary$$
5	4 1	wcel	$$wffy\in A$$
6	5 0	wnf	$$wffℲxy\in A$$
7	6 3	wal	$$wff\forall yℲxy\in A$$
8	2 7	wb	$$wff\left(\underset{\_}{Ⅎ}xA\leftrightarrow \forall yℲxy\in A\right)$$