Theorem eubii 2054

Description: Introduce unique existential quantifier to both sides of an equivalence. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 6-Oct-2016.)

Hypothesis

Ref	Expression
eubii.1	|- ( ph <-> ps )

Assertion

Ref	Expression
eubii	|- ( E! x ph <-> E! x ps )

Proof of Theorem eubii

Step	Hyp	Ref	Expression
1		eubii.1	. . . 4 |- ( ph <-> ps )
2	1	a1i 9	. . 3 |- ( T. -> ( ph <-> ps ) )
3	2	eubidv 2053	. 2 |- ( T. -> ( E! x ph <-> E! x ps ) )
4	3	mptru 1373	1 |- ( E! x ph <-> E! x ps )

Syntax hints:   <-> wb 105   T. wtru 1365   E!weu 2045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-eu 2048

This theorem is referenced by:  cbveu  2069  2eu7  2139  reubiia  2682  cbvreu  2727  reuv  2782  euxfr2dc  2949  euxfrdc  2950  2reuswapdc  2968  reuun2  3446  zfnuleu  4157  copsexg  4277  funeu2  5284  funcnv3  5320  fneu2  5363  tz6.12  5586  f1ompt  5713  fsn  5734  climreu  11462  divalgb  12090  gsum0g  13039  txcn  14511