![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-nnfnt | Structured version Visualization version GIF version |
Description: A variable is nonfree in a formula if and only if it is nonfree in its negation. The foward implication is intuitionistically valid (and that direction is sufficient for the purpose of recursively proving that some formulas have a given variable not free in them, like bj-nnfim 36729). Intuitionistically, ⊢ (Ⅎ'𝑥¬ 𝜑 ↔ Ⅎ'𝑥¬ ¬ 𝜑). See nfnt 1854. (Contributed by BJ, 28-Jul-2023.) |
Ref | Expression |
---|---|
bj-nnfnt | ⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥 ¬ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eximal 1779 | . . 3 ⊢ ((∃𝑥𝜑 → 𝜑) ↔ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)) | |
2 | alimex 1828 | . . 3 ⊢ ((𝜑 → ∀𝑥𝜑) ↔ (∃𝑥 ¬ 𝜑 → ¬ 𝜑)) | |
3 | 1, 2 | anbi12ci 629 | . 2 ⊢ (((∃𝑥𝜑 → 𝜑) ∧ (𝜑 → ∀𝑥𝜑)) ↔ ((∃𝑥 ¬ 𝜑 → ¬ 𝜑) ∧ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))) |
4 | df-bj-nnf 36707 | . 2 ⊢ (Ⅎ'𝑥𝜑 ↔ ((∃𝑥𝜑 → 𝜑) ∧ (𝜑 → ∀𝑥𝜑))) | |
5 | df-bj-nnf 36707 | . 2 ⊢ (Ⅎ'𝑥 ¬ 𝜑 ↔ ((∃𝑥 ¬ 𝜑 → ¬ 𝜑) ∧ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))) | |
6 | 3, 4, 5 | 3bitr4i 303 | 1 ⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥 ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1535 ∃wex 1776 Ⅎ'wnnf 36706 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-bj-nnf 36707 |
This theorem is referenced by: bj-nnfnth 36726 bj-equsexvwd 36764 |
Copyright terms: Public domain | W3C validator |