Definition df-nfc 2884

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 2882	. 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  2885  nfcr  2887  nfcrALT  2888  nfcd  2890  nfcriOLD  2892  nfcriOLDOLD  2893  nfceqdf  2897  nfceqdfOLD  2898  nfceqi  2899  nfnfc1  2905  nfeqd  2912  nfnfc  2914  drnfc1  2921  drnfc1OLD  2922  drnfc2  2923  drnfc2OLD  2924  dfnfc2  4895  nfnid  5335  nfriotadw  7326  bj-nfcf  35466