Theorem eubii 2619

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

Syntax hints:   ↔ wb 209  ∃!weu 2602

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-mo 2573  df-eu 2603

This theorem is referenced by:  cbveu  2641  2eu7  2691  2eu8  2692  exists1  2694  reubiia  3383  cbvreu  3415  reuv  3491  reurab  3673  euxfr2w  3692  euxfrw  3693  euxfr2  3694  euxfr  3695  2reuswap  3718  2reuswap2  3719  2reu5lem1  3727  reuun2  4286  euelss  4293  reusv2lem4  5373  copsexgw  5473  copsexgwOLD  5474  copsexg  5475  funeu2  6563  funcnv3  6607  fneu2  6647  tz6.12  6906  f1ompt  7107  fsn  7132  oeeu  8588  dfac5lem1  10106  dfac5lem5  10110  zmin  12967  climreu  15606  divalglem10  16459  divalgb  16461  dfinito2  18059  dftermo2  18060  txcn  23751  nbusgredgeu0  29658  adjeu  32181  reuxfrdf  32777  bnj130  35206  bnj207  35213  bnj864  35254  reueqi  36589  reueqbii  36590  bj-nuliota  37580  bj-axseprep  37598  poimirlem25  38183  poimirlem27  38185  dfsuccl4  39012  tfsconcatlem  43954  dfac5prim  45590  modelac8prim  45592  permac8prim  45614  aiotaval  47720  afveu  47778  tz6.12-1-afv  47799  tz6.12-afv2  47865  tz6.12-1-afv2  47866  pairreueq  48147  reutru  49466