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

Metamath Proof Explorer

Theorem dfnf5

Description: Characterization of nonfreeness in a formula in terms of its extension. (Contributed by BJ, 19-Mar-2021)

Ref Expression
Assertion dfnf5 ⊢ Ⅎ x φ ↔ x | φ = V ∨ x | φ = ∅

Proof

Step Hyp Ref Expression
1 nf3 ⊢ Ⅎ x φ ↔ ∀ x φ ∨ ∀ x ¬ φ
2 abv ⊢ x | φ = V ↔ ∀ x φ
3 ab0 ⊢ x | φ = ∅ ↔ ∀ x ¬ φ
4 2 3 orbi12i ⊢ x | φ = V ∨ x | φ = ∅ ↔ ∀ x φ ∨ ∀ x ¬ φ
5 1 4 bitr4i ⊢ Ⅎ x φ ↔ x | φ = V ∨ x | φ = ∅