Theorem eubii 2583

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 1912. (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 1849	. . 3 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)
3	1	mobii 2546	. . 3 ⊢ (∃*𝑥𝜑 ↔ ∃*𝑥𝜓)
4	2, 3	anbi12i 627	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜓 ∧ ∃*𝑥𝜓))
5		df-eu 2567	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
6		df-eu 2567	. 2 ⊢ (∃!𝑥𝜓 ↔ (∃𝑥𝜓 ∧ ∃*𝑥𝜓))
7	4, 5, 6	3bitr4i 302	1 ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃wex 1780  ∃*wmo 2536  ∃!weu 2566

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-mo 2538  df-eu 2567

This theorem is referenced by:  cbveuwOLD  2606  cbveu  2607  2eu7  2657  2eu8  2658  exists1  2660  reubiia  3356  reuanidOLD  3362  cbvreuwOLD  3385  cbvreu  3395  reuv  3467  euxfr2w  3665  euxfrw  3666  euxfr2  3667  euxfr  3668  2reuswap  3691  2reuswap2  3692  2reu5lem1  3700  reuun2  4260  euelss  4267  reusv2lem4  5341  copsexgw  5428  copsexg  5429  funeu2  6504  funcnv3  6548  fneu2  6590  tz6.12  6844  f1ompt  7035  fsn  7057  oeeu  8497  dfac5lem1  9972  dfac5lem5  9976  zmin  12777  climreu  15356  divalglem10  16202  divalgb  16204  dfinito2  17807  dftermo2  17808  txcn  22875  nbusgredgeu0  27965  adjeu  30480  reuxfrdf  31068  bnj130  33094  bnj207  33101  bnj864  33142  reurab  33909  bj-nuliota  35326  poimirlem25  35900  poimirlem27  35902  aiotaval  44927  afveu  44985  tz6.12-1-afv  45006  tz6.12-afv2  45072  tz6.12-1-afv2  45073  pairreueq  45302  reutru  46491