Theorem eubii 2589

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 2588	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓))
2		eubii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1804	1 ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)

Syntax hints:   ↔ wb 207  ∃!weu 2572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-mo 2543  df-eu 2573

This theorem is referenced by:  cbveu  2611  2eu7  2661  2eu8  2662  exists1  2664  reubiia  3351  cbvreu  3383  reuv  3459  reurab  3642  euxfr2w  3661  euxfrw  3662  euxfr2  3663  euxfr  3664  2reuswap  3687  2reuswap2  3688  2reu5lem1  3696  reuun2  4253  euelss  4260  reusv2lem4  5330  copsexgw  5430  copsexgwOLD  5431  copsexg  5432  funeu2  6511  funcnv3  6555  fneu2  6596  tz6.12  6851  f1ompt  7052  fsn  7077  oeeu  8529  dfac5lem1  10036  dfac5lem5  10040  zmin  12885  climreu  15509  divalglem10  16362  divalgb  16364  dfinito2  17961  dftermo2  17962  txcn  23609  nbusgredgeu0  29455  adjeu  31978  reuxfrdf  32578  bnj130  35056  bnj207  35063  bnj864  35104  reueqi  36417  reueqbii  36418  bj-nuliota  37410  bj-axseprep  37427  poimirlem25  38012  poimirlem27  38014  dfsuccl4  38841  tfsconcatlem  43781  dfac5prim  45434  modelac8prim  45436  permac8prim  45458  aiotaval  47558  afveu  47616  tz6.12-1-afv  47637  tz6.12-afv2  47703  tz6.12-1-afv2  47704  pairreueq  47985  reutru  49294