This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )