Theorem eubii 2578

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

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

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 2533  df-eu 2562

This theorem is referenced by:  cbveu  2600  2eu7  2651  2eu8  2652  exists1  2654  reubiia  3361  reuanidOLD  3367  cbvreu  3397  reuv  3476  reurab  3672  euxfr2w  3691  euxfrw  3692  euxfr2  3693  euxfr  3694  2reuswap  3717  2reuswap2  3718  2reu5lem1  3726  reuun2  4288  euelss  4295  reusv2lem4  5356  copsexgw  5450  copsexg  5451  funeu2  6542  funcnv3  6586  fneu2  6629  tz6.12  6883  f1ompt  7083  fsn  7107  oeeu  8567  dfac5lem1  10076  dfac5lem5  10080  zmin  12903  climreu  15522  divalglem10  16372  divalgb  16374  dfinito2  17965  dftermo2  17966  txcn  23513  nbusgredgeu0  29295  adjeu  31818  reuxfrdf  32420  bnj130  34864  bnj207  34871  bnj864  34912  reueqi  36177  reueqbii  36178  bj-nuliota  37045  poimirlem25  37639  poimirlem27  37641  tfsconcatlem  43325  dfac5prim  44980  modelac8prim  44982  permac8prim  45004  aiotaval  47096  afveu  47154  tz6.12-1-afv  47175  tz6.12-afv2  47241  tz6.12-1-afv2  47242  pairreueq  47511  reutru  48792