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 34096). Intuitionistically, ⊢ (Ⅎ'𝑥¬ 𝜑 ↔ Ⅎ'𝑥¬ ¬ 𝜑). See nfnt 1855. (Contributed by BJ, 28-Jul-2023.) |
Ref | Expression |
---|---|
bj-nnfnt | ⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥 ¬ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eximal 1782 | . . 3 ⊢ ((∃𝑥𝜑 → 𝜑) ↔ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)) | |
2 | alimex 1830 | . . 3 ⊢ ((𝜑 → ∀𝑥𝜑) ↔ (∃𝑥 ¬ 𝜑 → ¬ 𝜑)) | |
3 | 1, 2 | anbi12ci 629 | . 2 ⊢ (((∃𝑥𝜑 → 𝜑) ∧ (𝜑 → ∀𝑥𝜑)) ↔ ((∃𝑥 ¬ 𝜑 → ¬ 𝜑) ∧ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))) |
4 | df-bj-nnf 34077 | . 2 ⊢ (Ⅎ'𝑥𝜑 ↔ ((∃𝑥𝜑 → 𝜑) ∧ (𝜑 → ∀𝑥𝜑))) | |
5 | df-bj-nnf 34077 | . 2 ⊢ (Ⅎ'𝑥 ¬ 𝜑 ↔ ((∃𝑥 ¬ 𝜑 → ¬ 𝜑) ∧ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))) | |
6 | 3, 4, 5 | 3bitr4i 305 | 1 ⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥 ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∀wal 1534 ∃wex 1779 Ⅎ'wnnf 34076 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1780 df-bj-nnf 34077 |
This theorem is referenced by: bj-nnfnth 34093 |
Copyright terms: Public domain | W3C validator |