Theorem eubii 2584

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

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

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 2539  df-eu 2568

This theorem is referenced by:  cbveu  2606  2eu7  2657  2eu8  2658  exists1  2660  reubiia  3366  reuanidOLD  3372  cbvreuwOLD  3394  cbvreu  3407  reuv  3489  reurab  3684  euxfr2w  3703  euxfrw  3704  euxfr2  3705  euxfr  3706  2reuswap  3729  2reuswap2  3730  2reu5lem1  3738  reuun2  4300  euelss  4307  reusv2lem4  5371  copsexgw  5465  copsexg  5466  funeu2  6562  funcnv3  6606  fneu2  6649  tz6.12  6901  f1ompt  7101  fsn  7125  oeeu  8615  dfac5lem1  10137  dfac5lem5  10141  zmin  12960  climreu  15572  divalglem10  16421  divalgb  16423  dfinito2  18016  dftermo2  18017  txcn  23564  nbusgredgeu0  29347  adjeu  31870  reuxfrdf  32472  bnj130  34905  bnj207  34912  bnj864  34953  reueqi  36207  reueqbii  36208  bj-nuliota  37075  poimirlem25  37669  poimirlem27  37671  tfsconcatlem  43360  dfac5prim  45015  modelac8prim  45017  aiotaval  47124  afveu  47182  tz6.12-1-afv  47203  tz6.12-afv2  47269  tz6.12-1-afv2  47270  pairreueq  47524  reutru  48783