| 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 1784 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 2890 | . 2 wff Ⅎ𝑥𝐴 |
| 4 | vy | . . . . . 6 setvar 𝑦 | |
| 5 | 4 | cv 1539 | . . . . 5 class 𝑦 |
| 6 | 5, 2 | wcel 2108 | . . . 4 wff 𝑦 ∈ 𝐴 |
| 7 | 6, 1 | wnf 1783 | . . 3 wff Ⅎ𝑥 𝑦 ∈ 𝐴 |
| 8 | 7, 4 | wal 1538 | . 2 wff ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴 |
| 9 | 3, 8 | wb 206 | 1 wff (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) |
| Colors of variables: wff setvar class |
| This definition is referenced by: nfci 2893 nfcr 2895 nfcrALT 2896 nfcd 2898 nfceqdf 2901 nfceqi 2902 nfnfc1 2908 nfeqd 2916 nfnfc 2918 drnfc1 2925 drnfc2 2926 dfnfc2 4929 nfnid 5375 nfriotadw 7396 bj-nfcf 36924 |
| Copyright terms: Public domain | W3C validator |