Theorem eubii 2670

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 1911. (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 2631	. . 3 ⊢ (∃*𝑥𝜑 ↔ ∃*𝑥𝜓)
4	2, 3	anbi12i 628	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜓 ∧ ∃*𝑥𝜓))
5		df-eu 2654	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
6		df-eu 2654	. 2 ⊢ (∃!𝑥𝜓 ↔ (∃𝑥𝜓 ∧ ∃*𝑥𝜓))
7	4, 5, 6	3bitr4i 305	1 ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)

Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wex 1780  ∃*wmo 2620  ∃!weu 2653

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-mo 2622  df-eu 2654

This theorem is referenced by:  cbveuw  2690  cbveu  2691  2eu7  2743  2eu8  2744  exists1  2746  reuanid  3328  reubiia  3390  cbvreuw  3443  cbvreu  3447  reuv  3521  euxfr2w  3711  euxfrw  3712  euxfr2  3713  euxfr  3714  2reuswap  3737  2reuswap2  3738  2reu5lem1  3746  reuun2  4286  euelss  4290  reusv2lem4  5302  copsexgw  5381  copsexg  5382  funeu2  6381  funcnv3  6424  fneu2  6462  tz6.12  6693  f1ompt  6875  fsn  6897  oeeu  8229  dfac5lem1  9549  dfac5lem5  9553  zmin  12345  climreu  14913  divalglem10  15753  divalgb  15755  txcn  22234  nbusgredgeu0  27150  adjeu  29666  reuxfrdf  30255  bnj130  32146  bnj207  32153  bnj864  32194  bj-nuliota  34353  poimirlem25  34932  poimirlem27  34934  aiotaval  43313  afveu  43372  tz6.12-1-afv  43393  tz6.12-afv2  43459  tz6.12-1-afv2  43460  pairreueq  43692