Theorem nf4

Description: Alternate definition of non-freeness. This definition uses only primitive symbols ( -> , -. , A. ). (Contributed by BJ, 16-Sep-2021)

	Ref	Expression
Assertion	nf4	⊢ ( Ⅎ 𝑥 𝜑 ↔ ( ¬ ∀ 𝑥 𝜑 → ∀ 𝑥 ¬ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		nf3	⊢ ( Ⅎ 𝑥 𝜑 ↔ ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 ¬ 𝜑 ) )
2		df-or	⊢ ( ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 ¬ 𝜑 ) ↔ ( ¬ ∀ 𝑥 𝜑 → ∀ 𝑥 ¬ 𝜑 ) )
3	1 2	bitri	⊢ ( Ⅎ 𝑥 𝜑 ↔ ( ¬ ∀ 𝑥 𝜑 → ∀ 𝑥 ¬ 𝜑 ) )