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	|- ( F/_ x A <-> A. y F/ x y e. A )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		cA	|- A
2	0 1	wnfc	|- F/_ x A
3		vy	|- y
4	3	cv	|- y
5	4 1	wcel	|- y e. A
6	5 0	wnf	|- F/ x y e. A
7	6 3	wal	|- A. y F/ x y e. A
8	2 7	wb	|- ( F/_ x A <-> A. y F/ x y e. A )