Metamath Proof Explorer

Theorem bj-moeub

Description: Uniqueness is equivalent to existence being equivalent to unique existence. (Contributed by BJ, 14-Oct-2022)

Ref Expression
Assertion bj-moeub 
|- ( E* x ph <-> ( E. x ph <-> E! x ph ) )

Proof

Step Hyp Ref Expression
1 moeu 
 |-  ( E* x ph <-> ( E. x ph -> E! x ph ) )
2 euex 
 |-  ( E! x ph -> E. x ph )
3 impbi 
 |-  ( ( E. x ph -> E! x ph ) -> ( ( E! x ph -> E. x ph ) -> ( E. x ph <-> E! x ph ) ) )
4 2 3 mpi 
 |-  ( ( E. x ph -> E! x ph ) -> ( E. x ph <-> E! x ph ) )
5 biimp 
 |-  ( ( E. x ph <-> E! x ph ) -> ( E. x ph -> E! x ph ) )
6 4 5 impbii 
 |-  ( ( E. x ph -> E! x ph ) <-> ( E. x ph <-> E! x ph ) )
7 1 6 bitri 
 |-  ( E* x ph <-> ( E. x ph <-> E! x ph ) )