Theorem ralfal

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

	Ref	Expression
Hypothesis	ralfal.1	|- F/_ x A
Assertion	ralfal	|- ( A = (/) <-> A. x e. A F. )

Proof

Step	Hyp	Ref	Expression
1		ralfal.1	|- F/_ x A
2		df-fal	|- ( F. <-> -. T. )
3	2	ralbii	|- ( A. x e. A F. <-> A. x e. A -. T. )
4		ralnex	|- ( A. x e. A -. T. <-> -. E. x e. A T. )
5	3 4	bitri	|- ( A. x e. A F. <-> -. E. x e. A T. )
6		rextru	|- ( E. x x e. A <-> E. x e. A T. )
7	6	notbii	|- ( -. E. x x e. A <-> -. E. x e. A T. )
8	1	neq0f	|- ( -. A = (/) <-> E. x x e. A )
9	8	con1bii	|- ( -. E. x x e. A <-> A = (/) )
10	5 7 9	3bitr2ri	|- ( A = (/) <-> A. x e. A F. )