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\phi \leftrightarrow \left(\left\{x|\phi \right\}=\mathrm{V}\vee \left\{x|\phi \right\}=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		nf3	$$⊢Ⅎx\phi \leftrightarrow \left(\forall x\phi \vee \forall x\neg \phi \right)$$
2		abv	$$⊢\left\{x|\phi \right\}=\mathrm{V}\leftrightarrow \forall x\phi$$
3		ab0	$$⊢\left\{x|\phi \right\}=\varnothing \leftrightarrow \forall x\neg \phi$$
4	2 3	orbi12i	$$⊢\left(\left\{x|\phi \right\}=\mathrm{V}\vee \left\{x|\phi \right\}=\varnothing \right)\leftrightarrow \left(\forall x\phi \vee \forall x\neg \phi \right)$$
5	1 4	bitr4i	$$⊢Ⅎx\phi \leftrightarrow \left(\left\{x|\phi \right\}=\mathrm{V}\vee \left\{x|\phi \right\}=\varnothing \right)$$