Description: A variable is nonfree in a proposition if and only if it is so in its negation. (Contributed by BJ, 6-May-2019) (Proof shortened by Wolf Lammen, 6-Oct-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nfnbi | |- ( F/ x ph <-> F/ x -. ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exnal | |- ( E. x -. ph <-> -. A. x ph ) |
|
| 2 | 1 | imbi1i | |- ( ( E. x -. ph -> A. x -. ph ) <-> ( -. A. x ph -> A. x -. ph ) ) |
| 3 | df-nf | |- ( F/ x -. ph <-> ( E. x -. ph -> A. x -. ph ) ) |
|
| 4 | nf4 | |- ( F/ x ph <-> ( -. A. x ph -> A. x -. ph ) ) |
|
| 5 | 2 3 4 | 3bitr4ri | |- ( F/ x ph <-> F/ x -. ph ) |