Theorem eubii 2586

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	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
eubii	⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)

Proof of Theorem eubii

Step	Hyp	Ref	Expression
1		eubi 2585	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓))
2		eubii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1799	1 ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)

Syntax hints:   ↔ wb 206  ∃!weu 2569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2540  df-eu 2570

This theorem is referenced by:  cbveu  2608  2eu7  2659  2eu8  2660  exists1  2662  reubiia  3359  cbvreu  3393  reuv  3471  reurab  3661  euxfr2w  3680  euxfrw  3681  euxfr2  3682  euxfr  3683  2reuswap  3706  2reuswap2  3707  2reu5lem1  3715  reuun2  4279  euelss  4286  reusv2lem4  5348  copsexgw  5446  copsexg  5447  funeu2  6526  funcnv3  6570  fneu2  6611  tz6.12  6866  f1ompt  7065  fsn  7090  oeeu  8541  dfac5lem1  10045  dfac5lem5  10049  zmin  12869  climreu  15491  divalglem10  16341  divalgb  16343  dfinito2  17939  dftermo2  17940  txcn  23582  nbusgredgeu0  29453  adjeu  31977  reuxfrdf  32577  bnj130  35050  bnj207  35057  bnj864  35098  reueqi  36405  reueqbii  36406  bj-nuliota  37305  bj-axseprep  37322  poimirlem25  37896  poimirlem27  37898  dfsuccl4  38725  tfsconcatlem  43693  dfac5prim  45346  modelac8prim  45348  permac8prim  45370  aiotaval  47455  afveu  47513  tz6.12-1-afv  47534  tz6.12-afv2  47600  tz6.12-1-afv2  47601  pairreueq  47870  reutru  49163