Theorem eubii 2095

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

This proof depends on syntax axioms:   <-> wb 105   T. wtru 1403   E!weu 2086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-eu 2089

This theorem is used by:  cbveu  2110  2eu7  2181  reubiia  2738  cbvreu  2784  reuv  2841  euxfr2dc  3011  euxfrdc  3012  2reuswapdc  3030  reuun2  3516  zfnuleu  4259  copsexg  4386  funeu2  5406  funcnv3  5446  fneu2  5491  tz6.12  5726  f1ompt  5862  fsn  5883  climreu  12088  divalgb  12717  gzsum0  13772  txcn  15501  alseubii  17380