Theorem eubii 2579

Description: Introduce unique existential quantifier to both sides of an equivalence. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 6-Oct-2016.) Avoid ax-5 1910. (Revised by Wolf Lammen, 27-Sep-2023.)

Hypothesis

Ref	Expression
eubii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
eubii	⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)

Proof of Theorem eubii

Step	Hyp	Ref	Expression
1		eubii.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2	1	exbii 1848	. . 3 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)
3	1	mobii 2542	. . 3 ⊢ (∃*𝑥𝜑 ↔ ∃*𝑥𝜓)
4	2, 3	anbi12i 628	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜓 ∧ ∃*𝑥𝜓))
5		df-eu 2563	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
6		df-eu 2563	. 2 ⊢ (∃!𝑥𝜓 ↔ (∃𝑥𝜓 ∧ ∃*𝑥𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1779  ∃*wmo 2532  ∃!weu 2562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2534  df-eu 2563

This theorem is referenced by:  cbveu  2601  2eu7  2652  2eu8  2653  exists1  2655  reubiia  3363  reuanidOLD  3369  cbvreuwOLD  3389  cbvreu  3400  reuv  3479  reurab  3675  euxfr2w  3694  euxfrw  3695  euxfr2  3696  euxfr  3697  2reuswap  3720  2reuswap2  3721  2reu5lem1  3729  reuun2  4291  euelss  4298  reusv2lem4  5359  copsexgw  5453  copsexg  5454  funeu2  6545  funcnv3  6589  fneu2  6632  tz6.12  6886  f1ompt  7086  fsn  7110  oeeu  8570  dfac5lem1  10083  dfac5lem5  10087  zmin  12910  climreu  15529  divalglem10  16379  divalgb  16381  dfinito2  17972  dftermo2  17973  txcn  23520  nbusgredgeu0  29302  adjeu  31825  reuxfrdf  32427  bnj130  34871  bnj207  34878  bnj864  34919  reueqi  36184  reueqbii  36185  bj-nuliota  37052  poimirlem25  37646  poimirlem27  37648  tfsconcatlem  43332  dfac5prim  44987  modelac8prim  44989  permac8prim  45011  aiotaval  47100  afveu  47158  tz6.12-1-afv  47179  tz6.12-afv2  47245  tz6.12-1-afv2  47246  pairreueq  47515  reutru  48796