Theorem mo0sn

Description: Two ways of expressing "at most one" element in a class. (Contributed by Zhi Wang, 19-Sep-2024)

	Ref	Expression
Assertion	mo0sn	|- ( E* x x e. A <-> ( A = (/) \/ E. y A = { y } ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	|- F/ z x e. A
2		nfv	|- F/ x z e. A
3		eleq1w	|- ( x = z -> ( x e. A <-> z e. A ) )
4	1 2 3	cbvmow	|- ( E* x x e. A <-> E* z z e. A )
5		neq0	|- ( -. A = (/) <-> E. z z e. A )
6	5	anbi1i	|- ( ( -. A = (/) /\ E* z z e. A ) <-> ( E. z z e. A /\ E* z z e. A ) )
7		df-eu	|- ( E! z z e. A <-> ( E. z z e. A /\ E* z z e. A ) )
8		eu6	|- ( E! z z e. A <-> E. y A. z ( z e. A <-> z = y ) )
9	6 7 8	3bitr2i	|- ( ( -. A = (/) /\ E* z z e. A ) <-> E. y A. z ( z e. A <-> z = y ) )
10		dfcleq	|- ( A = { y } <-> A. z ( z e. A <-> z e. { y } ) )
11		velsn	|- ( z e. { y } <-> z = y )
12	11	bibi2i	|- ( ( z e. A <-> z e. { y } ) <-> ( z e. A <-> z = y ) )
13	12	albii	|- ( A. z ( z e. A <-> z e. { y } ) <-> A. z ( z e. A <-> z = y ) )
14	10 13	sylbbr	|- ( A. z ( z e. A <-> z = y ) -> A = { y } )
15	14	eximi	|- ( E. y A. z ( z e. A <-> z = y ) -> E. y A = { y } )
16	9 15	sylbi	|- ( ( -. A = (/) /\ E* z z e. A ) -> E. y A = { y } )
17	16	expcom	|- ( E* z z e. A -> ( -. A = (/) -> E. y A = { y } ) )
18	17	orrd	|- ( E* z z e. A -> ( A = (/) \/ E. y A = { y } ) )
19		mo0	|- ( A = (/) -> E* z z e. A )
20		mosn	|- ( A = { y } -> E* z z e. A )
21	20	exlimiv	|- ( E. y A = { y } -> E* z z e. A )
22	19 21	jaoi	|- ( ( A = (/) \/ E. y A = { y } ) -> E* z z e. A )
23	18 22	impbii	|- ( E* z z e. A <-> ( A = (/) \/ E. y A = { y } ) )
24	4 23	bitri	|- ( E* x x e. A <-> ( A = (/) \/ E. y A = { y } ) )