Theorem bj-nnfnt 34549

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

Assertion

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

Proof of Theorem bj-nnfnt

Step	Hyp	Ref	Expression
1		eximal 1789	. . 3 ⊢ ((∃𝑥𝜑 → 𝜑) ↔ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
2		alimex 1837	. . 3 ⊢ ((𝜑 → ∀𝑥𝜑) ↔ (∃𝑥 ¬ 𝜑 → ¬ 𝜑))
3	1, 2	anbi12ci 631	. 2 ⊢ (((∃𝑥𝜑 → 𝜑) ∧ (𝜑 → ∀𝑥𝜑)) ↔ ((∃𝑥 ¬ 𝜑 → ¬ 𝜑) ∧ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)))
4		df-bj-nnf 34533	. 2 ⊢ (Ⅎ'𝑥𝜑 ↔ ((∃𝑥𝜑 → 𝜑) ∧ (𝜑 → ∀𝑥𝜑)))
5		df-bj-nnf 34533	. 2 ⊢ (Ⅎ'𝑥 ¬ 𝜑 ↔ ((∃𝑥 ¬ 𝜑 → ¬ 𝜑) ∧ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)))
6	3, 4, 5	3bitr4i 306	1 ⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥 ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1540  ∃wex 1786  Ⅎ'wnnf 34532

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-bj-nnf 34533

This theorem is referenced by:  bj-nnfnth  34552