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		stdpc4	$$⊢\forall x\neg \phi \to \left[y/x\right]\neg \phi$$
2		sbn1	$$⊢\left[y/x\right]\neg \phi \to \neg \left[y/x\right]\phi$$
3	1 2	syl	$$⊢\forall x\neg \phi \to \neg \left[y/x\right]\phi$$
4		df-clab	$$⊢y\in \left\{x|\phi \right\}\leftrightarrow \left[y/x\right]\phi$$
5	3 4	sylnibr	$$⊢\forall x\neg \phi \to \neg y\in \left\{x|\phi \right\}$$
6	5	eq0rdv	$$⊢\forall x\neg \phi \to \left\{x|\phi \right\}=\varnothing$$