Theorem eubii 2015

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 2014	. 2 |- ( T. -> ( E! x ph <-> E! x ps ) )
4	3	mptru 1344	1 |- ( E! x ph <-> E! x ps )

Syntax hints:   <-> wb 104   T. wtru 1336   E!weu 2006

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-eu 2009

This theorem is referenced by:  cbveu  2030  2eu7  2100  reubiia  2641  cbvreu  2678  reuv  2731  euxfr2dc  2897  euxfrdc  2898  2reuswapdc  2916  reuun2  3390  zfnuleu  4088  copsexg  4203  funeu2  5193  funcnv3  5229  fneu2  5272  tz6.12  5493  f1ompt  5615  fsn  5636  climreu  11176  divalgb  11797  txcn  12635