Metamath Proof Explorer


Theorem eubii

Description: Introduce unique existential quantifier to both sides of an equivalence. (Contributed by NM, 9-Jul-1994) (Revised by Mario Carneiro, 6-Oct-2016) Avoid ax-5 . (Revised by Wolf Lammen, 27-Sep-2023)

Ref Expression
Hypothesis eubii.1
|- ( ph <-> ps )
Assertion eubii
|- ( E! x ph <-> E! x ps )

Proof

Step Hyp Ref Expression
1 eubii.1
 |-  ( ph <-> ps )
2 1 exbii
 |-  ( E. x ph <-> E. x ps )
3 1 mobii
 |-  ( E* x ph <-> E* x ps )
4 2 3 anbi12i
 |-  ( ( E. x ph /\ E* x ph ) <-> ( E. x ps /\ E* x ps ) )
5 df-eu
 |-  ( E! x ph <-> ( E. x ph /\ E* x ph ) )
6 df-eu
 |-  ( E! x ps <-> ( E. x ps /\ E* x ps ) )
7 4 5 6 3bitr4i
 |-  ( E! x ph <-> E! x ps )