Metamath Proof Explorer

Theorem moeuex

Description: Uniqueness implies that existence is equivalent to unique existence. (Contributed by BJ, 7-Oct-2022)

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

Proof

Step Hyp Ref Expression
1 df-eu 
 |-  ( E! x ph <-> ( E. x ph /\ E* x ph ) )
2 1 rbaibr 
 |-  ( E* x ph -> ( E. x ph <-> E! x ph ) )