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

Metamath Proof Explorer

Theorem nf3

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

Ref Expression
Assertion nf3 ⊢ Ⅎ x φ ↔ ∀ x φ ∨ ∀ x ¬ φ

Proof

Step Hyp Ref Expression
1 nf2 ⊢ Ⅎ x φ ↔ ∀ x φ ∨ ¬ ∃ x φ
2 alnex ⊢ ∀ x ¬ φ ↔ ¬ ∃ x φ
3 2 orbi2i ⊢ ∀ x φ ∨ ∀ x ¬ φ ↔ ∀ x φ ∨ ¬ ∃ x φ
4 1 3 bitr4i ⊢ Ⅎ x φ ↔ ∀ x φ ∨ ∀ x ¬ φ