Theorem eubii 2612

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

Syntax hints:   ↔ wb 208  ∃!weu 2595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-mo 2566  df-eu 2596

This theorem is referenced by:  cbveu  2634  2eu7  2684  2eu8  2685  exists1  2687  reubiia  3374  cbvreu  3406  reuv  3482  reurab  3664  euxfr2w  3683  euxfrw  3684  euxfr2  3685  euxfr  3686  2reuswap  3709  2reuswap2  3710  2reu5lem1  3718  reuun2  4277  euelss  4284  reusv2lem4  5358  copsexgw  5458  copsexgwOLD  5459  copsexg  5460  funeu2  6547  funcnv3  6591  fneu2  6632  tz6.12  6891  f1ompt  7092  fsn  7117  oeeu  8573  dfac5lem1  10079  dfac5lem5  10083  zmin  12945  climreu  15583  divalglem10  16436  divalgb  16438  dfinito2  18036  dftermo2  18037  txcn  23686  nbusgredgeu0  29569  adjeu  32092  reuxfrdf  32690  bnj130  35169  bnj207  35176  bnj864  35217  reueqi  36549  reueqbii  36550  bj-nuliota  37542  bj-axseprep  37559  poimirlem25  38144  poimirlem27  38146  dfsuccl4  38973  tfsconcatlem  43913  dfac5prim  45566  modelac8prim  45568  permac8prim  45590  aiotaval  47689  afveu  47747  tz6.12-1-afv  47768  tz6.12-afv2  47834  tz6.12-1-afv2  47835  pairreueq  48116  reutru  49425