Metamath Proof Explorer

Theorem modom2

Description: Two ways to express "at most one". (Contributed by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion modom2 
|- ( E* x x e. A <-> A ~<_ 1o )

Proof

Step Hyp Ref Expression
1 modom 
 |-  ( E* x x e. A <-> { x | x e. A } ~<_ 1o )
2 abid2 
 |-  { x | x e. A } = A
3 2 breq1i 
 |-  ( { x | x e. A } ~<_ 1o <-> A ~<_ 1o )
4 1 3 bitri 
 |-  ( E* x x e. A <-> A ~<_ 1o )