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  4257  copsexg  4384  funeu2  5403  funcnv3  5443  fneu2  5488  tz6.12  5723  f1ompt  5859  fsn  5880  climreu  12063  divalgb  12692  gzsum0  13713  txcn  15376  alseubii  17173