This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nf2

Description: Alternate definition of nonfreeness. (Contributed by BJ, 16-Sep-2021)

Ref Expression
Assertion nf2 ⊢ Ⅎ x φ ↔ ∀ x φ ∨ ¬ ∃ x φ

Proof

Step Hyp Ref Expression
1 df-nf ⊢ Ⅎ x φ ↔ ∃ x φ → ∀ x φ
2 imor ⊢ ∃ x φ → ∀ x φ ↔ ¬ ∃ x φ ∨ ∀ x φ
3 orcom ⊢ ¬ ∃ x φ ∨ ∀ x φ ↔ ∀ x φ ∨ ¬ ∃ x φ
4 1 2 3 3bitri ⊢ Ⅎ x φ ↔ ∀ x φ ∨ ¬ ∃ x φ