Theorem eubii 2586

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

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃wex 1782  ∃*wmo 2539  ∃!weu 2569

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-mo 2541  df-eu 2570

This theorem is referenced by:  cbveuwOLD  2609  cbveu  2610  2eu7  2660  2eu8  2661  exists1  2663  reuanid  3299  reubiia  3325  cbvreuwOLD  3378  cbvreu  3382  reuv  3459  euxfr2w  3656  euxfrw  3657  euxfr2  3658  euxfr  3659  2reuswap  3682  2reuswap2  3683  2reu5lem1  3691  reuun2  4249  euelss  4256  reusv2lem4  5325  copsexgw  5405  copsexg  5406  funeu2  6467  funcnv3  6511  fneu2  6553  tz6.12  6806  f1ompt  6994  fsn  7016  oeeu  8443  dfac5lem1  9888  dfac5lem5  9892  zmin  12693  climreu  15274  divalglem10  16120  divalgb  16122  dfinito2  17727  dftermo2  17728  txcn  22786  nbusgredgeu0  27744  adjeu  30260  reuxfrdf  30848  bnj130  32863  bnj207  32870  bnj864  32911  reurab  33683  bj-nuliota  35237  poimirlem25  35811  poimirlem27  35813  aiotaval  44598  afveu  44656  tz6.12-1-afv  44677  tz6.12-afv2  44743  tz6.12-1-afv2  44744  pairreueq  44973  reutru  46162