Theorem eubii 2578

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1779  ∃*wmo 2531  ∃!weu 2561

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2533  df-eu 2562

This theorem is referenced by:  cbveu  2600  2eu7  2651  2eu8  2652  exists1  2654  reubiia  3358  reuanidOLD  3364  cbvreu  3394  reuv  3473  reurab  3669  euxfr2w  3688  euxfrw  3689  euxfr2  3690  euxfr  3691  2reuswap  3714  2reuswap2  3715  2reu5lem1  3723  reuun2  4284  euelss  4291  reusv2lem4  5351  copsexgw  5445  copsexg  5446  funeu2  6526  funcnv3  6570  fneu2  6611  tz6.12  6865  f1ompt  7065  fsn  7089  oeeu  8544  dfac5lem1  10052  dfac5lem5  10056  zmin  12879  climreu  15498  divalglem10  16348  divalgb  16350  dfinito2  17941  dftermo2  17942  txcn  23489  nbusgredgeu0  29271  adjeu  31791  reuxfrdf  32393  bnj130  34837  bnj207  34844  bnj864  34885  reueqi  36150  reueqbii  36151  bj-nuliota  37018  poimirlem25  37612  poimirlem27  37614  tfsconcatlem  43298  dfac5prim  44953  modelac8prim  44955  permac8prim  44977  aiotaval  47069  afveu  47127  tz6.12-1-afv  47148  tz6.12-afv2  47214  tz6.12-1-afv2  47215  pairreueq  47484  reutru  48765