Theorem eubii 2585

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

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

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 2540  df-eu 2569

This theorem is referenced by:  cbveu  2607  2eu7  2658  2eu8  2659  exists1  2661  reubiia  3387  reuanidOLD  3393  cbvreuwOLD  3415  cbvreu  3428  reuv  3510  reurab  3707  euxfr2w  3726  euxfrw  3727  euxfr2  3728  euxfr  3729  2reuswap  3752  2reuswap2  3753  2reu5lem1  3761  reuun2  4325  euelss  4332  reusv2lem4  5401  copsexgw  5495  copsexg  5496  funeu2  6592  funcnv3  6636  fneu2  6679  tz6.12  6931  f1ompt  7131  fsn  7155  oeeu  8641  dfac5lem1  10163  dfac5lem5  10167  zmin  12986  climreu  15592  divalglem10  16439  divalgb  16441  dfinito2  18048  dftermo2  18049  txcn  23634  nbusgredgeu0  29385  adjeu  31908  reuxfrdf  32510  bnj130  34888  bnj207  34895  bnj864  34936  reueqi  36190  reueqbii  36191  bj-nuliota  37058  poimirlem25  37652  poimirlem27  37654  tfsconcatlem  43349  dfac5prim  45007  modelac8prim  45009  aiotaval  47107  afveu  47165  tz6.12-1-afv  47186  tz6.12-afv2  47252  tz6.12-1-afv2  47253  pairreueq  47497  reutru  48724