Definition df-nfc 2877

Description: Define the not-free predicate for classes. This is read "𝑥 is not free in 𝐴". Not-free means that the value of 𝑥 cannot affect the value of 𝐴, e.g., any occurrence of 𝑥 in 𝐴 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 1778 for wffs; see that definition for more information. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
df-nfc	⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴

Allowed substitution hint:   𝐴(𝑥)

Detailed syntax breakdown of Definition df-nfc

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar 𝑥
2		cA	. . 3 class 𝐴
3	1, 2	wnfc 2875	. 2 wff Ⅎ𝑥𝐴
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1532	. . . . 5 class 𝑦
6	5, 2	wcel 2098	. . . 4 wff 𝑦 ∈ 𝐴
7	6, 1	wnf 1777	. . 3 wff Ⅎ𝑥 𝑦 ∈ 𝐴
8	7, 4	wal 1531	. 2 wff ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴
9	3, 8	wb 205	1 wff (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)

This definition is referenced by:  nfci  2878  nfcr  2880  nfcrALT  2881  nfcd  2883  nfcriOLD  2885  nfcriOLDOLD  2886  nfceqdf  2890  nfceqdfOLD  2891  nfceqi  2892  nfnfc1  2898  nfeqd  2905  nfnfc  2907  drnfc1  2914  drnfc1OLD  2915  drnfc2  2916  drnfc2OLD  2917  dfnfc2  4923  nfnid  5363  nfriotadw  7365  bj-nfcf  36259