![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-nfc | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
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 (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |