Theorem eubii 2584

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 1918. (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 1855	. . 3 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)
3	1	mobii 2547	. . 3 ⊢ (∃*𝑥𝜑 ↔ ∃*𝑥𝜓)
4	2, 3	anbi12i 630	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜓 ∧ ∃*𝑥𝜓))
5		df-eu 2568	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
6		df-eu 2568	. 2 ⊢ (∃!𝑥𝜓 ↔ (∃𝑥𝜓 ∧ ∃*𝑥𝜓))
7	4, 5, 6	3bitr4i 306	1 ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)

Syntax hints:   ↔ wb 209   ∧ wa 399  ∃wex 1787  ∃*wmo 2537  ∃!weu 2567

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-mo 2539  df-eu 2568

This theorem is referenced by:  cbveuwOLD  2607  cbveu  2608  2eu7  2658  2eu8  2659  exists1  2661  reuanid  3246  reubiia  3302  cbvreuw  3351  cbvreu  3356  reuv  3434  euxfr2w  3633  euxfrw  3634  euxfr2  3635  euxfr  3636  2reuswap  3659  2reuswap2  3660  2reu5lem1  3668  reuun2  4229  euelss  4236  reusv2lem4  5294  copsexgw  5373  copsexg  5374  funeu2  6406  funcnv3  6450  fneu2  6489  tz6.12  6740  f1ompt  6928  fsn  6950  oeeu  8331  dfac5lem1  9737  dfac5lem5  9741  zmin  12540  climreu  15117  divalglem10  15963  divalgb  15965  dfinito2  17509  dftermo2  17510  txcn  22523  nbusgredgeu0  27456  adjeu  29970  reuxfrdf  30558  bnj130  32567  bnj207  32574  bnj864  32615  reurab  33389  bj-nuliota  34965  poimirlem25  35539  poimirlem27  35541  aiotaval  44259  afveu  44317  tz6.12-1-afv  44338  tz6.12-afv2  44404  tz6.12-1-afv2  44405  pairreueq  44635  reutru  45824