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  3350  reuanidOLD  3356  cbvreu  3386  reuv  3465  reurab  3661  euxfr2w  3680  euxfrw  3681  euxfr2  3682  euxfr  3683  2reuswap  3706  2reuswap2  3707  2reu5lem1  3715  reuun2  4276  euelss  4283  reusv2lem4  5340  copsexgw  5433  copsexg  5434  funeu2  6508  funcnv3  6552  fneu2  6593  tz6.12  6846  f1ompt  7045  fsn  7069  oeeu  8521  dfac5lem1  10017  dfac5lem5  10021  zmin  12845  climreu  15463  divalglem10  16313  divalgb  16315  dfinito2  17910  dftermo2  17911  txcn  23511  nbusgredgeu0  29313  adjeu  31833  reuxfrdf  32435  bnj130  34841  bnj207  34848  bnj864  34889  reueqi  36163  reueqbii  36164  bj-nuliota  37031  poimirlem25  37625  poimirlem27  37627  tfsconcatlem  43309  dfac5prim  44964  modelac8prim  44966  permac8prim  44988  aiotaval  47079  afveu  47137  tz6.12-1-afv  47158  tz6.12-afv2  47224  tz6.12-1-afv2  47225  pairreueq  47494  reutru  48788