Theorem eubii 2630

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 1888. (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 1829	. . 3 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)
3	1	mobii 2586	. . 3 ⊢ (∃*𝑥𝜑 ↔ ∃*𝑥𝜓)
4	2, 3	anbi12i 626	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜓 ∧ ∃*𝑥𝜓))
5		df-eu 2612	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
6		df-eu 2612	. 2 ⊢ (∃!𝑥𝜓 ↔ (∃𝑥𝜓 ∧ ∃*𝑥𝜓))
7	4, 5, 6	3bitr4i 304	1 ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)

Syntax hints:   ↔ wb 207   ∧ wa 396  ∃wex 1761  ∃*wmo 2574  ∃!weu 2611

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-mo 2576  df-eu 2612

This theorem is referenced by:  cbveu  2655  2eu7  2715  2eu8  2716  exists1  2719  reuanid  3289  reubiia  3350  cbvreu  3401  reuv  3464  euxfr2  3650  euxfr  3651  2reuswap  3674  2reuswap2  3675  2reu5lem1  3683  reuun2  4210  euelss  4214  reusv2lem4  5198  copsexg  5278  funeu2  6256  funcnv3  6299  fneu2  6337  tz6.12  6566  f1ompt  6743  fsn  6765  oeeu  8084  dfac5lem1  9400  dfac5lem5  9404  zmin  12198  climreu  14752  divalglem10  15591  divalgb  15593  txcn  21923  nbusgredgeu0  26838  adjeu  29362  reuxfrdf  29952  bnj130  31767  bnj207  31774  bnj864  31815  bj-nuliota  33973  poimirlem25  34473  poimirlem27  34475  aiotaval  42835  afveu  42894  tz6.12-1-afv  42915  tz6.12-afv2  42981  tz6.12-1-afv2  42982  pairreueq  43180