Definition df-nfc 2885

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 1786 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 2883	. 2 wff Ⅎ𝑥𝐴
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1540	. . . . 5 class 𝑦
6	5, 2	wcel 2106	. . . 4 wff 𝑦 ∈ 𝐴
7	6, 1	wnf 1785	. . 3 wff Ⅎ𝑥 𝑦 ∈ 𝐴
8	7, 4	wal 1539	. 2 wff ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴
9	3, 8	wb 205	1 wff (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)

This definition is referenced by:  nfci  2886  nfcr  2888  nfcrALT  2889  nfcd  2891  nfcriOLD  2893  nfcriOLDOLD  2894  nfceqdf  2898  nfceqdfOLD  2899  nfceqi  2900  nfnfc1  2906  nfeqd  2913  nfnfc  2915  drnfc1  2922  drnfc1OLD  2923  drnfc2  2924  drnfc2OLD  2925  dfnfc2  4933  nfnid  5373  nfriotadw  7375  bj-nfcf  36106