Metamath Proof Explorer

Theorem mobi

Description: Equivalence theorem for the at-most-one quantifier. (Contributed by BJ, 7-Oct-2022) (Proof shortened by Wolf Lammen, 18-Feb-2023)

Ref Expression
Assertion mobi 
|- ( A. x ( ph <-> ps ) -> ( E* x ph <-> E* x ps ) )

Proof

Step Hyp Ref Expression
1 albiim 
 |-  ( A. x ( ph <-> ps ) <-> ( A. x ( ph -> ps ) /\ A. x ( ps -> ph ) ) )
2 moim 
 |-  ( A. x ( ps -> ph ) -> ( E* x ph -> E* x ps ) )
3 moim 
 |-  ( A. x ( ph -> ps ) -> ( E* x ps -> E* x ph ) )
4 2 3 impbid21d 
 |-  ( A. x ( ph -> ps ) -> ( A. x ( ps -> ph ) -> ( E* x ph <-> E* x ps ) ) )
5 4 imp 
 |-  ( ( A. x ( ph -> ps ) /\ A. x ( ps -> ph ) ) -> ( E* x ph <-> E* x ps ) )
6 1 5 sylbi 
 |-  ( A. x ( ph <-> ps ) -> ( E* x ph <-> E* x ps ) )