# Metamath Proof Explorer

## Theorem dfnf5

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

Ref Expression
Assertion dfnf5 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\left\{{x}|{\phi }\right\}=\mathrm{V}\vee \left\{{x}|{\phi }\right\}=\varnothing \right)$

### Proof

Step Hyp Ref Expression
1 nf3 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\vee \forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\right)$
2 abv ${⊢}\left\{{x}|{\phi }\right\}=\mathrm{V}↔\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
3 ab0 ${⊢}\left\{{x}|{\phi }\right\}=\varnothing ↔\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }$
4 2 3 orbi12i ${⊢}\left(\left\{{x}|{\phi }\right\}=\mathrm{V}\vee \left\{{x}|{\phi }\right\}=\varnothing \right)↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\vee \forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\right)$
5 1 4 bitr4i ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\left\{{x}|{\phi }\right\}=\mathrm{V}\vee \left\{{x}|{\phi }\right\}=\varnothing \right)$