Theorem eubii 2580

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1780  ∃*wmo 2533  ∃!weu 2563

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 207  df-an 396  df-ex 1781  df-mo 2535  df-eu 2564

This theorem is referenced by:  cbveu  2602  2eu7  2653  2eu8  2654  exists1  2656  reubiia  3353  cbvreu  3387  reuv  3465  reurab  3655  euxfr2w  3674  euxfrw  3675  euxfr2  3676  euxfr  3677  2reuswap  3700  2reuswap2  3701  2reu5lem1  3709  reuun2  4272  euelss  4279  reusv2lem4  5337  copsexgw  5428  copsexg  5429  funeu2  6507  funcnv3  6551  fneu2  6592  tz6.12  6846  f1ompt  7044  fsn  7068  oeeu  8518  dfac5lem1  10014  dfac5lem5  10018  zmin  12842  climreu  15463  divalglem10  16313  divalgb  16315  dfinito2  17910  dftermo2  17911  txcn  23541  nbusgredgeu0  29346  adjeu  31869  reuxfrdf  32470  bnj130  34886  bnj207  34893  bnj864  34934  reueqi  36231  reueqbii  36232  bj-nuliota  37099  poimirlem25  37693  poimirlem27  37695  tfsconcatlem  43377  dfac5prim  45031  modelac8prim  45033  permac8prim  45055  aiotaval  47134  afveu  47192  tz6.12-1-afv  47213  tz6.12-afv2  47279  tz6.12-1-afv2  47280  pairreueq  47549  reutru  48843