Definition df-nfc 2938

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 2936	. 2 wff Ⅎ𝑥𝐴
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1537	. . . . 5 class 𝑦
6	5, 2	wcel 2111	. . . 4 wff 𝑦 ∈ 𝐴
7	6, 1	wnf 1785	. . 3 wff Ⅎ𝑥 𝑦 ∈ 𝐴
8	7, 4	wal 1536	. 2 wff ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴
9	3, 8	wb 209	1 wff (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)

This definition is referenced by:  nfci  2939  nfcr  2941  nfcrALT  2942  nfcd  2944  nfcriOLD  2946  nfcriOLDOLD  2947  nfceqdf  2951  nfceqi  2952  nfnfc1  2958  nfeqd  2965  nfnfc  2967  drnfc1  2974  drnfc2  2975  dfnfc2  4822  nfnid  5241  nfriotadw  7101  bj-nfcf  34366