Theorem eubii 2582

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 1907. (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 1844	. . 3 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)
3	1	mobii 2545	. . 3 ⊢ (∃*𝑥𝜑 ↔ ∃*𝑥𝜓)
4	2, 3	anbi12i 628	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜓 ∧ ∃*𝑥𝜓))
5		df-eu 2566	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
6		df-eu 2566	. 2 ⊢ (∃!𝑥𝜓 ↔ (∃𝑥𝜓 ∧ ∃*𝑥𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1775  ∃*wmo 2535  ∃!weu 2565

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-mo 2537  df-eu 2566

This theorem is referenced by:  cbveu  2604  2eu7  2655  2eu8  2656  exists1  2658  reubiia  3384  reuanidOLD  3390  cbvreuwOLD  3412  cbvreu  3424  reuv  3507  reurab  3709  euxfr2w  3728  euxfrw  3729  euxfr2  3730  euxfr  3731  2reuswap  3754  2reuswap2  3755  2reu5lem1  3763  reuun2  4330  euelss  4337  reusv2lem4  5406  copsexgw  5500  copsexg  5501  funeu2  6593  funcnv3  6637  fneu2  6679  tz6.12  6931  f1ompt  7130  fsn  7154  oeeu  8639  dfac5lem1  10160  dfac5lem5  10164  zmin  12983  climreu  15588  divalglem10  16435  divalgb  16437  dfinito2  18056  dftermo2  18057  txcn  23649  nbusgredgeu0  29399  adjeu  31917  reuxfrdf  32518  bnj130  34866  bnj207  34873  bnj864  34914  reueqi  36170  reueqbii  36171  bj-nuliota  37039  poimirlem25  37631  poimirlem27  37633  tfsconcatlem  43325  aiotaval  47044  afveu  47102  tz6.12-1-afv  47123  tz6.12-afv2  47189  tz6.12-1-afv2  47190  pairreueq  47434  reutru  48652