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  5336  copsexgw  5436  copsexg  5437  funeu2  6516  funcnv3  6560  fneu2  6601  tz6.12  6856  f1ompt  7055  fsn  7080  oeeu  8530  dfac5lem1  10034  dfac5lem5  10038  zmin  12883  climreu  15507  divalglem10  16360  divalgb  16362  dfinito2  17959  dftermo2  17960  txcn  23600  nbusgredgeu0  29456  adjeu  31980  reuxfrdf  32580  bnj130  35037  bnj207  35044  bnj864  35085  reueqi  36392  reueqbii  36393  bj-nuliota  37377  bj-axseprep  37394  poimirlem25  37977  poimirlem27  37979  dfsuccl4  38806  tfsconcatlem  43779  dfac5prim  45432  modelac8prim  45434  permac8prim  45456  aiotaval  47540  afveu  47598  tz6.12-1-afv  47619  tz6.12-afv2  47685  tz6.12-1-afv2  47686  pairreueq  47967  reutru  49276