Theorem eubii 2492

Description: Introduce uniqueness 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 11	. . 3 |- ( T. -> ( ph <-> ps ) )
3	2	eubidv 2490	. 2 |- ( T. -> ( E! x ph <-> E! x ps ) )
4	3	trud 1493	1 |- ( E! x ph <-> E! x ps )

Syntax hints:   <-> wb 196   T. wtru 1484   E!weu 2470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-tru 1486  df-ex 1705  df-nf 1710  df-eu 2474

This theorem is referenced by:  cbveu  2505  2eu7  2559  2eu8  2560  reubiia  3127  cbvreu  3169  reuv  3221  euxfr2  3391  euxfr  3392  2reuswap  3410  2reu5lem1  3413  reuun2  3910  euelss  3914  zfnuleu  4786  reusv2lem4  4872  copsexg  4956  funeu2  5914  funcnv3  5959  fneu2  5996  tz6.12  6211  f1ompt  6382  fsn  6402  oeeu  7683  dfac5lem1  8946  dfac5lem5  8950  zmin  11784  climreu  14287  divalglem10  15125  divalgb  15127  txcn  21429  nbusgredgeu0  26270  adjeu  28748  2reuswap2  29328  bnj130  30944  bnj207  30951  bnj864  30992  bj-nuliota  33019  poimirlem25  33434  poimirlem27  33436  afveu  41233  tz6.12-1-afv  41254