Theorem modom

Description: Two ways to express "at most one". (Contributed by Stefan O'Rear, 28-Oct-2014)

	Ref	Expression
Assertion	modom	|- ( E* x ph <-> { x | ph } ~<_ 1o )

Proof

Step	Hyp	Ref	Expression
1		moeu	|- ( E* x ph <-> ( E. x ph -> E! x ph ) )
2		imor	|- ( ( E. x ph -> E! x ph ) <-> ( -. E. x ph \/ E! x ph ) )
3		abn0	|- ( { x | ph } =/= (/) <-> E. x ph )
4	3	necon1bbii	|- ( -. E. x ph <-> { x | ph } = (/) )
5		sdom1	|- ( { x | ph } ~< 1o <-> { x | ph } = (/) )
6	4 5	bitr4i	|- ( -. E. x ph <-> { x | ph } ~< 1o )
7		euen1	|- ( E! x ph <-> { x | ph } ~~ 1o )
8	6 7	orbi12i	|- ( ( -. E. x ph \/ E! x ph ) <-> ( { x | ph } ~< 1o \/ { x | ph } ~~ 1o ) )
9		brdom2	|- ( { x | ph } ~<_ 1o <-> ( { x | ph } ~< 1o \/ { x | ph } ~~ 1o ) )
10	8 9	bitr4i	|- ( ( -. E. x ph \/ E! x ph ) <-> { x | ph } ~<_ 1o )
11	1 2 10	3bitri	|- ( E* x ph <-> { x | ph } ~<_ 1o )