Theorem eubii 2063

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 2062	. 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 2054

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-eu 2057

This theorem is referenced by:  cbveu  2078  2eu7  2148  reubiia  2691  cbvreu  2736  reuv  2791  euxfr2dc  2958  euxfrdc  2959  2reuswapdc  2977  reuun2  3456  zfnuleu  4169  copsexg  4289  funeu2  5298  funcnv3  5337  fneu2  5382  tz6.12  5606  f1ompt  5733  fsn  5754  climreu  11641  divalgb  12269  gsum0g  13261  txcn  14780