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 1799	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 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 2539  df-eu 2569

This theorem is referenced by:  cbveu  2607  2eu7  2658  2eu8  2659  exists1  2661  reubiia  3349  cbvreu  3381  reuv  3458  reurab  3647  euxfr2w  3666  euxfrw  3667  euxfr2  3668  euxfr  3669  2reuswap  3692  2reuswap2  3693  2reu5lem1  3701  reuun2  4265  euelss  4272  reusv2lem4  5343  copsexgw  5443  copsexgwOLD  5444  copsexg  5445  funeu2  6524  funcnv3  6568  fneu2  6609  tz6.12  6864  f1ompt  7063  fsn  7088  oeeu  8539  dfac5lem1  10045  dfac5lem5  10049  zmin  12894  climreu  15518  divalglem10  16371  divalgb  16373  dfinito2  17970  dftermo2  17971  txcn  23591  nbusgredgeu0  29437  adjeu  31960  reuxfrdf  32560  bnj130  35016  bnj207  35023  bnj864  35064  reueqi  36371  reueqbii  36372  bj-nuliota  37364  bj-axseprep  37381  poimirlem25  37966  poimirlem27  37968  dfsuccl4  38795  tfsconcatlem  43764  dfac5prim  45417  modelac8prim  45419  permac8prim  45441  aiotaval  47543  afveu  47601  tz6.12-1-afv  47622  tz6.12-afv2  47688  tz6.12-1-afv2  47689  pairreueq  47970  reutru  49279