Theorem nfnbi

Description: A variable is nonfree in a proposition if and only if it is so in its negation. (Contributed by BJ, 6-May-2019) (Proof shortened by Wolf Lammen, 6-Oct-2024)

	Ref	Expression
Assertion	nfnbi	⊢ ( Ⅎ 𝑥 𝜑 ↔ Ⅎ 𝑥 ¬ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		exnal	⊢ ( ∃ 𝑥 ¬ 𝜑 ↔ ¬ ∀ 𝑥 𝜑 )
2	1	imbi1i	⊢ ( ( ∃ 𝑥 ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 ) ↔ ( ¬ ∀ 𝑥 𝜑 → ∀ 𝑥 ¬ 𝜑 ) )
3		df-nf	⊢ ( Ⅎ 𝑥 ¬ 𝜑 ↔ ( ∃ 𝑥 ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 ) )
4		nf4	⊢ ( Ⅎ 𝑥 𝜑 ↔ ( ¬ ∀ 𝑥 𝜑 → ∀ 𝑥 ¬ 𝜑 ) )
5	2 3 4	3bitr4ri	⊢ ( Ⅎ 𝑥 𝜑 ↔ Ⅎ 𝑥 ¬ 𝜑 )