Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  eubii Structured version   Visualization version   GIF version

Theorem eubii 2645
 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 1911. (Revised by Wolf Lammen, 27-Sep-2023.)
Hypothesis
Ref Expression
eubii.1 (𝜑𝜓)
Assertion
Ref Expression
eubii (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)

Proof of Theorem eubii
StepHypRef Expression
1 eubii.1 . . . 4 (𝜑𝜓)
21exbii 1849 . . 3 (∃𝑥𝜑 ↔ ∃𝑥𝜓)
31mobii 2606 . . 3 (∃*𝑥𝜑 ↔ ∃*𝑥𝜓)
42, 3anbi12i 629 . 2 ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜓 ∧ ∃*𝑥𝜓))
5 df-eu 2629 . 2 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
6 df-eu 2629 . 2 (∃!𝑥𝜓 ↔ (∃𝑥𝜓 ∧ ∃*𝑥𝜓))
74, 5, 63bitr4i 306 1 (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399  ∃wex 1781  ∃*wmo 2596  ∃!weu 2628 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-mo 2598  df-eu 2629 This theorem is referenced by:  cbveuwOLD  2667  cbveu  2668  2eu7  2720  2eu8  2721  exists1  2723  reuanid  3286  reubiia  3343  cbvreuw  3389  cbvreu  3394  reuv  3468  euxfr2w  3659  euxfrw  3660  euxfr2  3661  euxfr  3662  2reuswap  3685  2reuswap2  3686  2reu5lem1  3694  reuun2  4238  euelss  4242  reusv2lem4  5268  copsexgw  5347  copsexg  5348  funeu2  6351  funcnv3  6395  fneu2  6434  tz6.12  6669  f1ompt  6853  fsn  6875  oeeu  8215  dfac5lem1  9537  dfac5lem5  9541  zmin  12335  climreu  14908  divalglem10  15746  divalgb  15748  txcn  22241  nbusgredgeu0  27168  adjeu  29682  reuxfrdf  30272  bnj130  32271  bnj207  32278  bnj864  32319  bj-nuliota  34493  poimirlem25  35101  poimirlem27  35103  aiotaval  43693  afveu  43752  tz6.12-1-afv  43773  tz6.12-afv2  43839  tz6.12-1-afv2  43840  pairreueq  44070
 Copyright terms: Public domain W3C validator