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

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

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-mo 2540  df-eu 2569

This theorem is referenced by:  cbveuwOLD  2608  cbveu  2609  2eu7  2659  2eu8  2660  exists1  2662  reuanid  3256  reubiia  3316  cbvreuw  3365  cbvreu  3370  reuv  3448  euxfr2w  3650  euxfrw  3651  euxfr2  3652  euxfr  3653  2reuswap  3676  2reuswap2  3677  2reu5lem1  3685  reuun2  4245  euelss  4252  reusv2lem4  5319  copsexgw  5398  copsexg  5399  funeu2  6444  funcnv3  6488  fneu2  6528  tz6.12  6779  f1ompt  6967  fsn  6989  oeeu  8396  dfac5lem1  9810  dfac5lem5  9814  zmin  12613  climreu  15193  divalglem10  16039  divalgb  16041  dfinito2  17634  dftermo2  17635  txcn  22685  nbusgredgeu0  27638  adjeu  30152  reuxfrdf  30740  bnj130  32754  bnj207  32761  bnj864  32802  reurab  33576  bj-nuliota  35155  poimirlem25  35729  poimirlem27  35731  aiotaval  44474  afveu  44532  tz6.12-1-afv  44553  tz6.12-afv2  44619  tz6.12-1-afv2  44620  pairreueq  44850  reutru  46039