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  3330  reubiia  3392  cbvreuw  3445  cbvreu  3449  reuv  3523  euxfr2w  3713  euxfrw  3714  euxfr2  3715  euxfr  3716  2reuswap  3739  2reuswap2  3740  2reu5lem1  3748  reuun2  4288  euelss  4292  reusv2lem4  5304  copsexgw  5383  copsexg  5384  funeu2  6383  funcnv3  6426  fneu2  6464  tz6.12  6695  f1ompt  6877  fsn  6899  oeeu  8231  dfac5lem1  9551  dfac5lem5  9555  zmin  12347  climreu  14915  divalglem10  15755  divalgb  15757  txcn  22236  nbusgredgeu0  27152  adjeu  29668  reuxfrdf  30257  bnj130  32148  bnj207  32155  bnj864  32196  bj-nuliota  34352  poimirlem25  34919  poimirlem27  34921  aiotaval  43300  afveu  43359  tz6.12-1-afv  43380  tz6.12-afv2  43446  tz6.12-1-afv2  43447  pairreueq  43679