Theorem eubii 2064

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

Syntax hints:   <-> wb 105   T. wtru 1374   E!weu 2055

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-eu 2058

This theorem is referenced by:  cbveu  2079  2eu7  2150  reubiia  2694  cbvreu  2740  reuv  2796  euxfr2dc  2965  euxfrdc  2966  2reuswapdc  2984  reuun2  3464  zfnuleu  4184  copsexg  4306  funeu2  5316  funcnv3  5355  fneu2  5400  tz6.12  5627  f1ompt  5754  fsn  5775  climreu  11723  divalgb  12351  gsum0g  13343  txcn  14862