Theorem ralfal

Description: Two ways of expressing empty set. (Contributed by Glauco Siliprandi, 24-Jan-2024)

	Ref	Expression
Hypothesis	ralfal.1	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	ralfal	$$⊢A=\varnothing \leftrightarrow \forall x\in A\perp$$

Proof

Step	Hyp	Ref	Expression
1		ralfal.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		df-fal	$$⊢\perp \leftrightarrow \neg \top$$
3	2	ralbii	$$⊢\forall x\in A\perp \leftrightarrow \forall x\in A\neg \top$$
4		ralnex	$$⊢\forall x\in A\neg \top \leftrightarrow \neg \exists x\in A\top$$
5	3 4	bitri	$$⊢\forall x\in A\perp \leftrightarrow \neg \exists x\in A\top$$
6		rextru	$$⊢\exists xx\in A\leftrightarrow \exists x\in A\top$$
7	6	notbii	$$⊢\neg \exists xx\in A\leftrightarrow \neg \exists x\in A\top$$
8	1	neq0f	$$⊢\neg A=\varnothing \leftrightarrow \exists xx\in A$$
9	8	con1bii	$$⊢\neg \exists xx\in A\leftrightarrow A=\varnothing$$
10	5 7 9	3bitr2ri	$$⊢A=\varnothing \leftrightarrow \forall x\in A\perp$$