Theorem bj-ab0

Description: The class of sets verifying a falsity is the empty set (closed form of abf ). (Contributed by BJ, 24-Jul-2019) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ax-5	$$⊢\forall x\neg \phi \to \forall y\forall x\neg \phi$$
2		stdpc4	$$⊢\forall x\neg \phi \to \left[y/x\right]\neg \phi$$
3		sbn	$$⊢\left[y/x\right]\neg \phi \leftrightarrow \neg \left[y/x\right]\phi$$
4	2 3	sylib	$$⊢\forall x\neg \phi \to \neg \left[y/x\right]\phi$$
5		df-clab	$$⊢y\in \left\{x|\phi \right\}\leftrightarrow \left[y/x\right]\phi$$
6	4 5	sylnibr	$$⊢\forall x\neg \phi \to \neg y\in \left\{x|\phi \right\}$$
7	1 6	alrimih	$$⊢\forall x\neg \phi \to \forall y\neg y\in \left\{x|\phi \right\}$$
8		eq0	$$⊢\left\{x|\phi \right\}=\varnothing \leftrightarrow \forall y\neg y\in \left\{x|\phi \right\}$$
9	7 8	sylibr	$$⊢\forall x\neg \phi \to \left\{x|\phi \right\}=\varnothing$$