Theorem bj-nnfnt 36941

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 36947). Intuitionistically, ⊢ (Ⅎ'𝑥¬ 𝜑 ↔ Ⅎ'𝑥¬ ¬ 𝜑). See nfnt 1857. (Contributed by BJ, 28-Jul-2023.)

Assertion

Ref	Expression
bj-nnfnt	⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥 ¬ 𝜑)

Proof of Theorem bj-nnfnt

Step	Hyp	Ref	Expression
1		eximal 1783	. . 3 ⊢ ((∃𝑥𝜑 → 𝜑) ↔ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
2		alimex 1832	. . 3 ⊢ ((𝜑 → ∀𝑥𝜑) ↔ (∃𝑥 ¬ 𝜑 → ¬ 𝜑))
3	1, 2	anbi12ci 629	. 2 ⊢ (((∃𝑥𝜑 → 𝜑) ∧ (𝜑 → ∀𝑥𝜑)) ↔ ((∃𝑥 ¬ 𝜑 → ¬ 𝜑) ∧ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)))
4		df-bj-nnf 36925	. 2 ⊢ (Ⅎ'𝑥𝜑 ↔ ((∃𝑥𝜑 → 𝜑) ∧ (𝜑 → ∀𝑥𝜑)))
5		df-bj-nnf 36925	. 2 ⊢ (Ⅎ'𝑥 ¬ 𝜑 ↔ ((∃𝑥 ¬ 𝜑 → ¬ 𝜑) ∧ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)))
6	3, 4, 5	3bitr4i 303	1 ⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥 ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539  ∃wex 1780  Ⅎ'wnnf 36924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-bj-nnf 36925

This theorem is referenced by:  bj-nnfnth  36944  bj-equsexvwd  36982