Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-nnfnt Structured version   Visualization version   GIF version

Theorem bj-nnfnt 36723
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.)
Assertion
Ref Expression
bj-nnfnt (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥 ¬ 𝜑)

Proof of Theorem bj-nnfnt
StepHypRef Expression
1 eximal 1779 . . 3 ((∃𝑥𝜑𝜑) ↔ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
2 alimex 1828 . . 3 ((𝜑 → ∀𝑥𝜑) ↔ (∃𝑥 ¬ 𝜑 → ¬ 𝜑))
31, 2anbi12ci 629 . 2 (((∃𝑥𝜑𝜑) ∧ (𝜑 → ∀𝑥𝜑)) ↔ ((∃𝑥 ¬ 𝜑 → ¬ 𝜑) ∧ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)))
4 df-bj-nnf 36707 . 2 (Ⅎ'𝑥𝜑 ↔ ((∃𝑥𝜑𝜑) ∧ (𝜑 → ∀𝑥𝜑)))
5 df-bj-nnf 36707 . 2 (Ⅎ'𝑥 ¬ 𝜑 ↔ ((∃𝑥 ¬ 𝜑 → ¬ 𝜑) ∧ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)))
63, 4, 53bitr4i 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