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  3447  zfnuleu  4158  copsexg  4278  funeu2  5285  funcnv3  5321  fneu2  5366  tz6.12  5589  f1ompt  5716  fsn  5737  climreu  11479  divalgb  12107  gsum0g  13098  txcn  14595