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  3350  cbvreu  3382  reuv  3459  reurab  3648  euxfr2w  3667  euxfrw  3668  euxfr2  3669  euxfr  3670  2reuswap  3693  2reuswap2  3694  2reu5lem1  3702  reuun2  4266  euelss  4273  reusv2lem4  5339  copsexgw  5439  copsexg  5440  funeu2  6519  funcnv3  6563  fneu2  6604  tz6.12  6859  f1ompt  7058  fsn  7083  oeeu  8533  dfac5lem1  10039  dfac5lem5  10043  zmin  12888  climreu  15512  divalglem10  16365  divalgb  16367  dfinito2  17964  dftermo2  17965  txcn  23604  nbusgredgeu0  29454  adjeu  31978  reuxfrdf  32578  bnj130  35035  bnj207  35042  bnj864  35083  reueqi  36390  reueqbii  36391  bj-nuliota  37383  bj-axseprep  37400  poimirlem25  37983  poimirlem27  37985  dfsuccl4  38812  tfsconcatlem  43785  dfac5prim  45438  modelac8prim  45440  permac8prim  45462  aiotaval  47558  afveu  47616  tz6.12-1-afv  47637  tz6.12-afv2  47703  tz6.12-1-afv2  47704  pairreueq  47985  reutru  49294