Theorem eu0

Description: There is only one empty set. (Contributed by RP, 1-Oct-2023)

	Ref	Expression
Assertion	eu0	|- ( A. x -. x e. (/) /\ E! x A. y -. y e. x )

Proof

Step	Hyp	Ref	Expression
1		noel	|- -. x e. (/)
2	1	ax-gen	|- A. x -. x e. (/)
3		ax-nul	|- E. x A. y -. y e. x
4		nulmo	|- E* x A. y -. y e. x
5		df-eu	|- ( E! x A. y -. y e. x <-> ( E. x A. y -. y e. x /\ E* x A. y -. y e. x ) )
6	3 4 5	mpbir2an	|- E! x A. y -. y e. x
7	2 6	pm3.2i	|- ( A. x -. x e. (/) /\ E! x A. y -. y e. x )