Theorem ab0

Description: The class of sets verifying a property is the empty class if and only if that property is a contradiction. See also abn0 (from which it could be proved using as many essential proof steps but one fewer syntactic step, at the cost of depending on df-ne ). (Contributed by BJ, 19-Mar-2021) Avoid df-clel , ax-8 . (Revised by Gino Giotto, 30-Aug-2024) (Proof shortened by SN, 8-Sep-2024)

	Ref	Expression
Assertion	ab0	$$⊢\left\{x|\phi \right\}=\varnothing \leftrightarrow \forall x\neg \phi$$

Proof

Step	Hyp	Ref	Expression
1		abbi	$$⊢\forall x\left(\phi \leftrightarrow \perp \right)\leftrightarrow \left\{x|\phi \right\}=\left\{x|\perp \right\}$$
2		nbfal	$$⊢\neg \phi \leftrightarrow \left(\phi \leftrightarrow \perp \right)$$
3	2	albii	$$⊢\forall x\neg \phi \leftrightarrow \forall x\left(\phi \leftrightarrow \perp \right)$$
4		dfnul4	$$⊢\varnothing =\left\{x|\perp \right\}$$
5	4	eqeq2i	$$⊢\left\{x|\phi \right\}=\varnothing \leftrightarrow \left\{x|\phi \right\}=\left\{x|\perp \right\}$$
6	1 3 5	3bitr4ri	$$⊢\left\{x|\phi \right\}=\varnothing \leftrightarrow \forall x\neg \phi$$