Metamath Proof Explorer

Theorem reuen1

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

Ref Expression
Assertion reuen1 
|- ( E! x e. A ph <-> { x e. A | ph } ~~ 1o )

Proof

Step Hyp Ref Expression
1 reusn 
 |-  ( E! x e. A ph <-> E. y { x e. A | ph } = { y } )
2 en1 
 |-  ( { x e. A | ph } ~~ 1o <-> E. y { x e. A | ph } = { y } )
3 1 2 bitr4i 
 |-  ( E! x e. A ph <-> { x e. A | ph } ~~ 1o )