Theorem eubii 2585

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

Syntax hints:   ↔ wb 206  ∃!weu 2568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-mo 2539  df-eu 2569

This theorem is referenced by:  cbveu  2607  2eu7  2658  2eu8  2659  exists1  2661  reubiia  3357  cbvreu  3391  reuv  3469  reurab  3659  euxfr2w  3678  euxfrw  3679  euxfr2  3680  euxfr  3681  2reuswap  3704  2reuswap2  3705  2reu5lem1  3713  reuun2  4277  euelss  4284  reusv2lem4  5346  copsexgw  5438  copsexg  5439  funeu2  6518  funcnv3  6562  fneu2  6603  tz6.12  6858  f1ompt  7056  fsn  7080  oeeu  8531  dfac5lem1  10033  dfac5lem5  10037  zmin  12857  climreu  15479  divalglem10  16329  divalgb  16331  dfinito2  17927  dftermo2  17928  txcn  23570  nbusgredgeu0  29441  adjeu  31964  reuxfrdf  32565  bnj130  35030  bnj207  35037  bnj864  35078  reueqi  36383  reueqbii  36384  bj-nuliota  37258  poimirlem25  37846  poimirlem27  37848  dfsuccl4  38648  tfsconcatlem  43578  dfac5prim  45231  modelac8prim  45233  permac8prim  45255  aiotaval  47341  afveu  47399  tz6.12-1-afv  47420  tz6.12-afv2  47486  tz6.12-1-afv2  47487  pairreueq  47756  reutru  49049