Definition df-nfc 2889

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 1792 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 2887	. 2 wff Ⅎ𝑥𝐴
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1542	. . . . 5 class 𝑦
6	5, 2	wcel 2112	. . . 4 wff 𝑦 ∈ 𝐴
7	6, 1	wnf 1791	. . 3 wff Ⅎ𝑥 𝑦 ∈ 𝐴
8	7, 4	wal 1541	. 2 wff ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴
9	3, 8	wb 209	1 wff (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)

This definition is referenced by:  nfci  2890  nfcr  2892  nfcrALT  2893  nfcd  2895  nfcriOLD  2897  nfcriOLDOLD  2898  nfceqdf  2902  nfceqdfOLD  2903  nfceqi  2904  nfnfc1  2910  nfeqd  2917  nfnfc  2919  drnfc1  2926  drnfc1OLD  2927  drnfc2  2928  drnfc2OLD  2929  dfnfc2  4860  nfnid  5292  nfriotadw  7217  bj-nfcf  35013