Theorem eubii 2588

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 1909. (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 1846	. . 3 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)
3	1	mobii 2551	. . 3 ⊢ (∃*𝑥𝜑 ↔ ∃*𝑥𝜓)
4	2, 3	anbi12i 627	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜓 ∧ ∃*𝑥𝜓))
5		df-eu 2572	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
6		df-eu 2572	. 2 ⊢ (∃!𝑥𝜓 ↔ (∃𝑥𝜓 ∧ ∃*𝑥𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1777  ∃*wmo 2541  ∃!weu 2571

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-mo 2543  df-eu 2572

This theorem is referenced by:  cbveu  2610  2eu7  2661  2eu8  2662  exists1  2664  reubiia  3395  reuanidOLD  3401  cbvreuwOLD  3423  cbvreu  3435  reuv  3518  reurab  3723  euxfr2w  3742  euxfrw  3743  euxfr2  3744  euxfr  3745  2reuswap  3768  2reuswap2  3769  2reu5lem1  3777  reuun2  4344  euelss  4351  reusv2lem4  5419  copsexgw  5510  copsexg  5511  funeu2  6604  funcnv3  6648  fneu2  6690  tz6.12  6945  f1ompt  7145  fsn  7169  oeeu  8659  dfac5lem1  10192  dfac5lem5  10196  zmin  13009  climreu  15602  divalglem10  16450  divalgb  16452  dfinito2  18070  dftermo2  18071  txcn  23655  nbusgredgeu0  29403  adjeu  31921  reuxfrdf  32519  bnj130  34850  bnj207  34857  bnj864  34898  reueqi  36153  reueqbii  36154  bj-nuliota  37023  poimirlem25  37605  poimirlem27  37607  tfsconcatlem  43298  aiotaval  47010  afveu  47068  tz6.12-1-afv  47089  tz6.12-afv2  47155  tz6.12-1-afv2  47156  pairreueq  47384  reutru  48537