Theorem nfnbi

Description: A variable is non-free in a proposition if and only if it is so in its negation. (Contributed by BJ, 6-May-2019)

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

Proof

Step	Hyp	Ref	Expression
1		orcom	⊢ ( ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 ¬ 𝜑 ) ↔ ( ∀ 𝑥 ¬ 𝜑 ∨ ∀ 𝑥 𝜑 ) )
2		nf3	⊢ ( Ⅎ 𝑥 𝜑 ↔ ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 ¬ 𝜑 ) )
3		nf3	⊢ ( Ⅎ 𝑥 ¬ 𝜑 ↔ ( ∀ 𝑥 ¬ 𝜑 ∨ ∀ 𝑥 ¬ ¬ 𝜑 ) )
4		notnotb	⊢ ( 𝜑 ↔ ¬ ¬ 𝜑 )
5	4	albii	⊢ ( ∀ 𝑥 𝜑 ↔ ∀ 𝑥 ¬ ¬ 𝜑 )
6	5	orbi2i	⊢ ( ( ∀ 𝑥 ¬ 𝜑 ∨ ∀ 𝑥 𝜑 ) ↔ ( ∀ 𝑥 ¬ 𝜑 ∨ ∀ 𝑥 ¬ ¬ 𝜑 ) )
7	3 6	bitr4i	⊢ ( Ⅎ 𝑥 ¬ 𝜑 ↔ ( ∀ 𝑥 ¬ 𝜑 ∨ ∀ 𝑥 𝜑 ) )
8	1 2 7	3bitr4i	⊢ ( Ⅎ 𝑥 𝜑 ↔ Ⅎ 𝑥 ¬ 𝜑 )