Theorem eubii 2583

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

Syntax hints:   ↔ wb 206  ∃!weu 2566

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 2537  df-eu 2567

This theorem is referenced by:  cbveu  2605  2eu7  2656  2eu8  2657  exists1  2659  reubiia  3355  cbvreu  3389  reuv  3467  reurab  3657  euxfr2w  3676  euxfrw  3677  euxfr2  3678  euxfr  3679  2reuswap  3702  2reuswap2  3703  2reu5lem1  3711  reuun2  4275  euelss  4282  reusv2lem4  5344  copsexgw  5436  copsexg  5437  funeu2  6516  funcnv3  6560  fneu2  6601  tz6.12  6856  f1ompt  7054  fsn  7078  oeeu  8529  dfac5lem1  10031  dfac5lem5  10035  zmin  12855  climreu  15477  divalglem10  16327  divalgb  16329  dfinito2  17925  dftermo2  17926  txcn  23568  nbusgredgeu0  29390  adjeu  31913  reuxfrdf  32514  bnj130  34979  bnj207  34986  bnj864  35027  reueqi  36332  reueqbii  36333  bj-nuliota  37201  poimirlem25  37785  poimirlem27  37787  dfsuccl4  38587  tfsconcatlem  43520  dfac5prim  45173  modelac8prim  45175  permac8prim  45197  aiotaval  47283  afveu  47341  tz6.12-1-afv  47362  tz6.12-afv2  47428  tz6.12-1-afv2  47429  pairreueq  47698  reutru  48991