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  4168  copsexg  4288  funeu2  5297  funcnv3  5336  fneu2  5381  tz6.12  5604  f1ompt  5731  fsn  5752  climreu  11608  divalgb  12236  gsum0g  13228  txcn  14747