Metamath Proof Explorer


Theorem bj-nnfnt

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 ). Intuitionistically, |- ( F// x -. ph <-> F// x -. -. ph ) . See nfnt . (Contributed by BJ, 28-Jul-2023)

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

Proof

Step Hyp Ref Expression
1 eximal ( ( ∃ 𝑥 𝜑𝜑 ) ↔ ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 ) )
2 alimex ( ( 𝜑 → ∀ 𝑥 𝜑 ) ↔ ( ∃ 𝑥 ¬ 𝜑 → ¬ 𝜑 ) )
3 1 2 anbi12ci ( ( ( ∃ 𝑥 𝜑𝜑 ) ∧ ( 𝜑 → ∀ 𝑥 𝜑 ) ) ↔ ( ( ∃ 𝑥 ¬ 𝜑 → ¬ 𝜑 ) ∧ ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 ) ) )
4 df-bj-nnf ( Ⅎ' 𝑥 𝜑 ↔ ( ( ∃ 𝑥 𝜑𝜑 ) ∧ ( 𝜑 → ∀ 𝑥 𝜑 ) ) )
5 df-bj-nnf ( Ⅎ' 𝑥 ¬ 𝜑 ↔ ( ( ∃ 𝑥 ¬ 𝜑 → ¬ 𝜑 ) ∧ ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 ) ) )
6 3 4 5 3bitr4i ( Ⅎ' 𝑥 𝜑 ↔ Ⅎ' 𝑥 ¬ 𝜑 )