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 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 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 205   ∧ wa 397  ∃wex 1782  ∃*wmo 2533  ∃!weu 2563

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 398  df-ex 1783  df-mo 2535  df-eu 2564

This theorem is referenced by:  cbveuwOLD  2603  cbveu  2604  2eu7  2654  2eu8  2655  exists1  2657  reubiia  3384  reuanidOLD  3390  cbvreuwOLD  3413  cbvreu  3425  reuv  3501  reurab  3698  euxfr2w  3717  euxfrw  3718  euxfr2  3719  euxfr  3720  2reuswap  3743  2reuswap2  3744  2reu5lem1  3752  reuun2  4315  euelss  4322  reusv2lem4  5400  copsexgw  5491  copsexg  5492  funeu2  6575  funcnv3  6619  fneu2  6661  tz6.12  6917  f1ompt  7111  fsn  7133  oeeu  8603  dfac5lem1  10118  dfac5lem5  10122  zmin  12928  climreu  15500  divalglem10  16345  divalgb  16347  dfinito2  17953  dftermo2  17954  txcn  23130  nbusgredgeu0  28625  adjeu  31142  reuxfrdf  31731  bnj130  33885  bnj207  33892  bnj864  33933  bj-nuliota  35938  poimirlem25  36513  poimirlem27  36515  tfsconcatlem  42086  aiotaval  45803  afveu  45861  tz6.12-1-afv  45882  tz6.12-afv2  45948  tz6.12-1-afv2  45949  pairreueq  46178  reutru  47490