Metamath Proof Explorer


Theorem nf4

Description: Alternate definition of nonfreeness. 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 ( Ⅎ 𝑥 𝜑 ↔ ( ¬ ∀ 𝑥 𝜑 → ∀ 𝑥 ¬ 𝜑 ) )