![]() |
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 35624). Intuitionistically, ⊢ (Ⅎ'𝑥¬ 𝜑 ↔ Ⅎ'𝑥¬ ¬ 𝜑). See nfnt 1860. (Contributed by BJ, 28-Jul-2023.) |
Ref | Expression |
---|---|
bj-nnfnt | ⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥 ¬ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eximal 1785 | . . 3 ⊢ ((∃𝑥𝜑 → 𝜑) ↔ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)) | |
2 | alimex 1834 | . . 3 ⊢ ((𝜑 → ∀𝑥𝜑) ↔ (∃𝑥 ¬ 𝜑 → ¬ 𝜑)) | |
3 | 1, 2 | anbi12ci 629 | . 2 ⊢ (((∃𝑥𝜑 → 𝜑) ∧ (𝜑 → ∀𝑥𝜑)) ↔ ((∃𝑥 ¬ 𝜑 → ¬ 𝜑) ∧ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))) |
4 | df-bj-nnf 35602 | . 2 ⊢ (Ⅎ'𝑥𝜑 ↔ ((∃𝑥𝜑 → 𝜑) ∧ (𝜑 → ∀𝑥𝜑))) | |
5 | df-bj-nnf 35602 | . 2 ⊢ (Ⅎ'𝑥 ¬ 𝜑 ↔ ((∃𝑥 ¬ 𝜑 → ¬ 𝜑) ∧ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))) | |
6 | 3, 4, 5 | 3bitr4i 303 | 1 ⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥 ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∀wal 1540 ∃wex 1782 Ⅎ'wnnf 35601 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-bj-nnf 35602 |
This theorem is referenced by: bj-nnfnth 35621 bj-equsexvwd 35659 |
Copyright terms: Public domain | W3C validator |