Theorem eubii 2611

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

This proof depends on syntax axioms:   ↔ wb 209  ∃!weu 2594

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2565  df-eu 2595

This theorem is used by:  cbveu  2633  2eu7  2683  2eu8  2684  exists1  2686  reubiia  3373  cbvreu  3405  reuv  3479  reurab  3659  euxfr2w  3678  euxfrw  3679  euxfr2  3680  euxfr  3681  2reuswap  3704  2reuswap2  3705  2reu5lem1  3713  reuun2  4271  euelss  4278  reusv2lem4  5363  copsexgwOLD  5461  funeu2  6566  funcnv3  6610  fneu2  6650  tz6.12  6909  f1ompt  7111  fsn  7136  oeeu  8612  dfac5lem1  10202  dfac5lem5  10206  zmin  13071  climreu  15723  divalglem10  16572  divalgb  16574  dfinito2  18178  dftermo2  18179  txcn  23945  nbusgredgeu0  29949  adjeu  32491  reuxfrdf  33087  bnj130  35504  bnj207  35511  bnj864  35552  reueqi  36978  reueqbii  36979  bj-nuliota  37972  bj-axseprep  37990  poimirlem25  38563  poimirlem27  38565  dfsuccl4  39406  tfsconcatlem  44337  dfac5prim  45979  modelac8prim  45981  permac8prim  46003  aiotaval  48164  afveu  48222  tz6.12-1-afv  48243  tz6.12-afv2  48309  tz6.12-1-afv2  48310  pairreueq  48591  reutru  49913  alseubii  50927